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:  2f1fvneq  7281  isocnv  7351  isocnv3  7353  f1oiso2  7373  xpexr2  7942  f1o2ndf1  8148  fnwelem  8157  omword  8609  oeword  8629  swoso  8780  xpf1o  9180  zorn2lem6  10542  ltapr  11086  ltord1  11790  pc11  16919  imasaddfnlem  17574  imasaddflem  17576  pslem  18618  mgmhmpropd  18712  mhmpropd  18806  frmdsssubm  18875  ghmsub  19243  gasubg  19321  invrpropd  20419  znfld  21580  cygznlem3  21589  mplcoe5lem  22058  evlseu  22108  cpmatmcl  22726  tgclb  22978  innei  23134  txcn  23635  txflf  24015  qustgplem  24130  clmsub4  25140  cfilresi  25330  volcn  25642  itg1addlem4  25735  dvlip  26033  plymullem1  26254  lgsdir2  27375  lgsdchr  27400  brbtwn2  28921  axcontlem7  28986  frgrncvvdeqlem8  30326  nvaddsub4  30677  hhcno  31924  hhcnf  31925  unopf1o  31936  counop  31941  mndlactf1o  33036  mndractf1o  33037  afsval  34687  ontopbas  36430  onsuct0  36443  heicant  37663  ftc1anclem6  37706  equivbnd2  37800  ismtybndlem  37814  ismrer1  37846  iccbnd  37848  ghomco  37899  rngohomco  37982  rngoisocnv  37989  rngoisoco  37990  idlsubcl  38031  xihopellsmN  41257  dihopellsm  41258  f1o2d2  42274  dvconstbi  44358  ovolval5lem3  46674  imasetpreimafvbijlemf1  47396  fargshiftf1  47433  elpglem1  49285