Theorem anim12dan 620

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 610	. 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  7288  isocnv3  7290  f1oiso2  7310  xpexr2  7873  f1o2ndf1  8076  fnwelem  8085  omword  8509  oeword  8530  swoso  8682  xpf1o  9081  zorn2lem6  10425  ltapr  10970  ltord1  11677  pc11  16822  imasaddfnlem  17463  imasaddflem  17465  pslem  18509  mgmhmpropd  18637  mhmpropd  18731  frmdsssubm  18800  ghmsub  19170  gasubg  19248  invrpropd  20371  znfld  21532  cygznlem3  21541  mplcoe5lem  22011  evlseu  22055  cpmatmcl  22680  tgclb  22931  innei  23086  txcn  23587  txflf  23967  qustgplem  24082  clmsub4  25079  cfilresi  25268  volcn  25580  itg1addlem4  25673  dvlip  25971  plymullem1  26192  lgsdir2  27314  lgsdchr  27339  brbtwn2  28996  axcontlem7  29061  frgrncvvdeqlem8  30399  nvaddsub4  30751  hhcno  31998  hhcnf  31999  unopf1o  32010  counop  32015  mndlactf1o  33129  mndractf1o  33130  afsval  34855  ontopbas  36650  onsuct0  36663  heicant  37935  ftc1anclem6  37978  equivbnd2  38072  ismtybndlem  38086  ismrer1  38118  iccbnd  38120  ghomco  38171  rngohomco  38254  rngoisocnv  38261  rngoisoco  38262  idlsubcl  38303  xihopellsmN  41659  dihopellsm  41660  f1o2d2  42634  dvconstbi  44719  ovolval5lem3  47041  imasetpreimafvbijlemf1  47793  fargshiftf1  47830  upgrimtrlslem2  48294  elpglem1  50099