Theorem anim12dan 621

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  2f1fvneq  6996  isocnv  7062  isocnv3  7064  f1oiso2  7084  xpexr2  7606  f1o2ndf1  7801  fnwelem  7808  omword  8179  oeword  8199  swoso  8305  xpf1o  8663  zorn2lem6  9912  ltapr  10456  ltord1  11155  pc11  16206  imasaddfnlem  16793  imasaddflem  16795  pslem  17808  mhmpropd  17954  frmdsssubm  18018  ghmsub  18358  gasubg  18424  invrpropd  19444  znfld  20252  cygznlem3  20261  mplcoe5lem  20707  evlseu  20755  cpmatmcl  21324  tgclb  21575  innei  21730  txcn  22231  txflf  22611  qustgplem  22726  clmsub4  23711  cfilresi  23899  volcn  24210  itg1addlem4  24303  dvlip  24596  plymullem1  24811  lgsdir2  25914  lgsdchr  25939  brbtwn2  26699  axcontlem7  26764  frgrncvvdeqlem8  28091  nvaddsub4  28440  hhcno  29687  hhcnf  29688  unopf1o  29699  counop  29704  afsval  32052  ontopbas  33889  onsuct0  33902  heicant  35092  ftc1anclem6  35135  equivbnd2  35230  ismtybndlem  35244  ismrer1  35276  iccbnd  35278  ghomco  35329  rngohomco  35412  rngoisocnv  35419  rngoisoco  35420  idlsubcl  35461  xihopellsmN  38550  dihopellsm  38551  dvconstbi  41038  imasetpreimafvbijlemf1  43921  fargshiftf1  43958  mgmhmpropd  44405  elpglem1  45240