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  7338  isocnv3  7340  f1oiso2  7360  xpexr2  7931  f1o2ndf1  8133  mpof1o2d  8137  fnwelem  8143  omword  8579  oeword  8600  swoso  8753  xpf1o  9159  zorn2lem6  10580  ltapr  11131  ltord1  11843  pc11  17059  imasaddfnlem  17701  imasaddflem  17703  pslem  18747  mgmhmpropd  18888  mhmpropd  18988  frmdsssubm  19058  ghmsub  19439  gasubg  19517  invrpropd  20649  znfld  21867  cygznlem3  21876  mplcoe5lem  22349  evlseu  22393  cpmatmcl  23038  tgclb  23289  innei  23444  txcn  23946  txflf  24326  qustgplem  24441  clmsub4  25428  cfilresi  25617  volcn  25928  itg1addlem4  26021  dvlip  26314  plymullem1  26534  lgsdir2  27658  lgsdchr  27683  brbtwn2  29484  axcontlem7  29549  frgrncvvdeqlem8  30908  nvaddsub4  31260  hhcno  32507  hhcnf  32508  unopf1o  32519  counop  32524  mndlactf1o  33634  mndractf1o  33635  afsval  35346  ontopbas  37291  onsuct0  37304  heicant  38649  ftc1anclem6  38692  equivbnd2  38802  ismtybndlem  38816  ismrer1  38848  iccbnd  38850  ghomco  38901  rngohomco  38984  rngoisocnv  38991  rngoisoco  38992  idlsubcl  39033  xihopellsmN  42387  dihopellsm  42388  dvconstbi  45394  ovolval5lem3  47740  imasetpreimafvbijlemf1  48562  fargshiftf1  48599  upgrimtrlslem2  49079  elpglem1  50880