Theorem anim12dan 631

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 418	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		anim12dan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
4	3	ex 418	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
5	2, 4	anim12d 621	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
6	5	imp 412	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  isocnv  7361  isocnv3  7363  f1oiso2  7383  xpexr2  7955  f1o2ndf1  8160  mpof1o2d  8164  fnwelem  8170  omword  8606  oeword  8627  swoso  8780  xpf1o  9186  zorn2lem6  10606  ltapr  11157  ltord1  11869  pc11  17087  imasaddfnlem  17729  imasaddflem  17731  pslem  18775  mgmhmpropd  18916  mhmpropd  19016  frmdsssubm  19086  ghmsub  19467  gasubg  19546  invrpropd  20678  znfld  21896  cygznlem3  21905  mplcoe5lem  22378  evlseu  22422  cpmatmcl  23067  tgclb  23318  innei  23473  txcn  23975  txflf  24355  qustgplem  24470  clmsub4  25457  cfilresi  25646  volcn  25957  itg1addlem4  26050  dvlip  26343  plymullem1  26563  lgsdir2  27687  lgsdchr  27712  brbtwn2  29513  axcontlem7  29578  frgrncvvdeqlem8  30937  nvaddsub4  31289  hhcno  32536  hhcnf  32537  unopf1o  32548  counop  32553  mndlactf1o  33661  mndractf1o  33662  afsval  35373  ontopbas  37394  onsuct0  37407  heicant  38765  ftc1anclem6  38808  equivbnd2  38918  ismtybndlem  38932  ismrer1  38964  iccbnd  38966  ghomco  39017  rngohomco  39100  rngoisocnv  39107  rngoisoco  39108  idlsubcl  39149  xihopellsmN  42503  dihopellsm  42504  dvconstbi  45510  ovolval5lem3  47869  imasetpreimafvbijlemf1  48691  fargshiftf1  48728  upgrimtrlslem2  49208  elpglem1  51084