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  7326  isocnv3  7328  f1oiso2  7348  xpexr2  7914  f1o2ndf1  8116  mpof1o2d  8120  fnwelem  8126  omword  8556  oeword  8577  swoso  8730  xpf1o  9136  zorn2lem6  10551  ltapr  11102  ltord1  11812  pc11  17020  imasaddfnlem  17662  imasaddflem  17664  pslem  18708  mgmhmpropd  18849  mhmpropd  18949  frmdsssubm  19019  ghmsub  19400  gasubg  19478  invrpropd  20610  znfld  21828  cygznlem3  21837  mplcoe5lem  22310  evlseu  22354  cpmatmcl  22999  tgclb  23250  innei  23405  txcn  23907  txflf  24287  qustgplem  24402  clmsub4  25389  cfilresi  25578  volcn  25889  itg1addlem4  25982  dvlip  26275  plymullem1  26495  lgsdir2  27621  lgsdchr  27646  brbtwn2  29417  axcontlem7  29482  frgrncvvdeqlem8  30841  nvaddsub4  31193  hhcno  32440  hhcnf  32441  unopf1o  32452  counop  32457  mndlactf1o  33525  mndractf1o  33526  afsval  35238  ontopbas  37138  onsuct0  37151  heicant  38493  ftc1anclem6  38536  equivbnd2  38646  ismtybndlem  38660  ismrer1  38692  iccbnd  38694  ghomco  38745  rngohomco  38828  rngoisocnv  38835  rngoisoco  38836  idlsubcl  38877  xihopellsmN  42231  dihopellsm  42232  dvconstbi  45262  ovolval5lem3  47586  imasetpreimafvbijlemf1  48408  fargshiftf1  48445  upgrimtrlslem2  48925  elpglem1  50726