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  7273  isocnv3  7275  f1oiso2  7295  xpexr2  7858  f1o2ndf1  8061  fnwelem  8070  omword  8494  oeword  8514  swoso  8665  xpf1o  9062  zorn2lem6  10402  ltapr  10946  ltord1  11653  pc11  16802  imasaddfnlem  17442  imasaddflem  17444  pslem  18488  mgmhmpropd  18616  mhmpropd  18710  frmdsssubm  18779  ghmsub  19146  gasubg  19224  invrpropd  20346  znfld  21507  cygznlem3  21516  mplcoe5lem  21984  evlseu  22028  cpmatmcl  22644  tgclb  22895  innei  23050  txcn  23551  txflf  23931  qustgplem  24046  clmsub4  25043  cfilresi  25232  volcn  25544  itg1addlem4  25637  dvlip  25935  plymullem1  26156  lgsdir2  27278  lgsdchr  27303  brbtwn2  28894  axcontlem7  28959  frgrncvvdeqlem8  30297  nvaddsub4  30648  hhcno  31895  hhcnf  31896  unopf1o  31907  counop  31912  mndlactf1o  33022  mndractf1o  33023  afsval  34695  ontopbas  36483  onsuct0  36496  heicant  37705  ftc1anclem6  37748  equivbnd2  37842  ismtybndlem  37856  ismrer1  37888  iccbnd  37890  ghomco  37941  rngohomco  38024  rngoisocnv  38031  rngoisoco  38032  idlsubcl  38073  xihopellsmN  41363  dihopellsm  41364  f1o2d2  42341  dvconstbi  44441  ovolval5lem3  46766  imasetpreimafvbijlemf1  47518  fargshiftf1  47555  upgrimtrlslem2  48019  elpglem1  49826