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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  2f1fvneq  7206  isocnv  7274  isocnv3  7276  f1oiso2  7296  xpexr2  7855  f1o2ndf1  8053  fnwelem  8062  omword  8516  oeword  8536  swoso  8680  xpf1o  9082  zorn2lem6  10436  ltapr  10980  ltord1  11680  pc11  16751  imasaddfnlem  17409  imasaddflem  17411  pslem  18460  mhmpropd  18607  frmdsssubm  18670  ghmsub  19014  gasubg  19080  invrpropd  20125  znfld  20965  cygznlem3  20974  mplcoe5lem  21438  evlseu  21491  cpmatmcl  22066  tgclb  22318  innei  22474  txcn  22975  txflf  23355  qustgplem  23470  clmsub4  24467  cfilresi  24657  volcn  24968  itg1addlem4  25061  itg1addlem4OLD  25062  dvlip  25355  plymullem1  25573  lgsdir2  26676  lgsdchr  26701  brbtwn2  27852  axcontlem7  27917  frgrncvvdeqlem8  29248  nvaddsub4  29597  hhcno  30844  hhcnf  30845  unopf1o  30856  counop  30861  afsval  33275  ontopbas  34891  onsuct0  34904  heicant  36104  ftc1anclem6  36147  equivbnd2  36242  ismtybndlem  36256  ismrer1  36288  iccbnd  36290  ghomco  36341  rngohomco  36424  rngoisocnv  36431  rngoisoco  36432  idlsubcl  36473  xihopellsmN  39708  dihopellsm  39709  mhphf  40749  dvconstbi  42596  ovolval5lem3  44867  imasetpreimafvbijlemf1  45568  fargshiftf1  45605  mgmhmpropd  46051  elpglem1  47128