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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  2f1fvneq  7012  isocnv  7077  isocnv3  7079  f1oiso2  7099  xpexr2  7618  f1o2ndf1  7812  fnwelem  7819  omword  8190  oeword  8210  swoso  8316  xpf1o  8673  zorn2lem6  9917  ltapr  10461  ltord1  11160  pc11  16210  imasaddfnlem  16795  imasaddflem  16797  pslem  17810  mhmpropd  17956  frmdsssubm  18020  ghmsub  18360  gasubg  18426  invrpropd  19442  mplcoe5lem  20242  evlseu  20290  znfld  20701  cygznlem3  20710  cpmatmcl  21321  tgclb  21572  innei  21727  txcn  22228  txflf  22608  qustgplem  22723  clmsub4  23704  cfilresi  23892  volcn  24201  itg1addlem4  24294  dvlip  24584  plymullem1  24798  lgsdir2  25900  lgsdchr  25925  brbtwn2  26685  axcontlem7  26750  frgrncvvdeqlem8  28079  nvaddsub4  28428  hhcno  29675  hhcnf  29676  unopf1o  29687  counop  29692  afsval  31937  ontopbas  33771  onsuct0  33784  heicant  34921  ftc1anclem6  34966  equivbnd2  35064  ismtybndlem  35078  ismrer1  35110  iccbnd  35112  ghomco  35163  rngohomco  35246  rngoisocnv  35253  rngoisoco  35254  idlsubcl  35295  xihopellsmN  38384  dihopellsm  38385  dvconstbi  40659  imasetpreimafvbijlemf1  43558  fargshiftf1  43595  mgmhmpropd  44046  elpglem1  44807