Theorem anim12dan 619

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 609	. 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 207  df-an 396

This theorem is referenced by:  isocnv  7308  isocnv3  7310  f1oiso2  7330  xpexr2  7898  f1o2ndf1  8104  fnwelem  8113  omword  8537  oeword  8557  swoso  8708  xpf1o  9109  zorn2lem6  10461  ltapr  11005  ltord1  11711  pc11  16858  imasaddfnlem  17498  imasaddflem  17500  pslem  18538  mgmhmpropd  18632  mhmpropd  18726  frmdsssubm  18795  ghmsub  19163  gasubg  19241  invrpropd  20334  znfld  21477  cygznlem3  21486  mplcoe5lem  21953  evlseu  21997  cpmatmcl  22613  tgclb  22864  innei  23019  txcn  23520  txflf  23900  qustgplem  24015  clmsub4  25013  cfilresi  25202  volcn  25514  itg1addlem4  25607  dvlip  25905  plymullem1  26126  lgsdir2  27248  lgsdchr  27273  brbtwn2  28839  axcontlem7  28904  frgrncvvdeqlem8  30242  nvaddsub4  30593  hhcno  31840  hhcnf  31841  unopf1o  31852  counop  31857  mndlactf1o  32978  mndractf1o  32979  afsval  34669  ontopbas  36423  onsuct0  36436  heicant  37656  ftc1anclem6  37699  equivbnd2  37793  ismtybndlem  37807  ismrer1  37839  iccbnd  37841  ghomco  37892  rngohomco  37975  rngoisocnv  37982  rngoisoco  37983  idlsubcl  38024  xihopellsmN  41255  dihopellsm  41256  f1o2d2  42228  dvconstbi  44330  ovolval5lem3  46659  imasetpreimafvbijlemf1  47409  fargshiftf1  47446  upgrimtrlslem2  47909  elpglem1  49704