Theorem anim12dan 618

Description: Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011.)

Hypotheses

Ref	Expression
anim12dan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
anim12dan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
anim12dan	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏))

Proof of Theorem anim12dan

Step	Hyp	Ref	Expression
1		anim12dan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		anim12dan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
4	3	ex 412	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
5	2, 4	anim12d 608	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
6	5	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  2f1fvneq  7264  isocnv  7332  isocnv3  7334  f1oiso2  7354  xpexr2  7921  f1o2ndf1  8121  fnwelem  8130  omword  8584  oeword  8604  swoso  8751  xpf1o  9155  zorn2lem6  10516  ltapr  11060  ltord1  11762  pc11  16840  imasaddfnlem  17501  imasaddflem  17503  pslem  18555  mgmhmpropd  18649  mhmpropd  18740  frmdsssubm  18804  ghmsub  19169  gasubg  19244  invrpropd  20346  znfld  21481  cygznlem3  21490  mplcoe5lem  21964  evlseu  22016  cpmatmcl  22608  tgclb  22860  innei  23016  txcn  23517  txflf  23897  qustgplem  24012  clmsub4  25020  cfilresi  25210  volcn  25522  itg1addlem4  25615  itg1addlem4OLD  25616  dvlip  25913  plymullem1  26135  lgsdir2  27250  lgsdchr  27275  brbtwn2  28703  axcontlem7  28768  frgrncvvdeqlem8  30103  nvaddsub4  30454  hhcno  31701  hhcnf  31702  unopf1o  31713  counop  31718  afsval  34239  ontopbas  35848  onsuct0  35861  heicant  37063  ftc1anclem6  37106  equivbnd2  37200  ismtybndlem  37214  ismrer1  37246  iccbnd  37248  ghomco  37299  rngohomco  37382  rngoisocnv  37389  rngoisoco  37390  idlsubcl  37431  xihopellsmN  40664  dihopellsm  40665  f1o2d2  41644  dvconstbi  43694  ovolval5lem3  45965  imasetpreimafvbijlemf1  46667  fargshiftf1  46704  elpglem1  48065