Theorem anim12dan 622

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 612	. 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  7072  isocnv  7139  isocnv3  7141  f1oiso2  7161  xpexr2  7697  f1o2ndf1  7891  fnwelem  7898  omword  8298  oeword  8318  swoso  8424  xpf1o  8808  zorn2lem6  10115  ltapr  10659  ltord1  11358  pc11  16433  imasaddfnlem  17033  imasaddflem  17035  pslem  18078  mhmpropd  18224  frmdsssubm  18288  ghmsub  18630  gasubg  18696  invrpropd  19716  znfld  20525  cygznlem3  20534  mplcoe5lem  20996  evlseu  21043  cpmatmcl  21616  tgclb  21867  innei  22022  txcn  22523  txflf  22903  qustgplem  23018  clmsub4  24003  cfilresi  24192  volcn  24503  itg1addlem4  24596  itg1addlem4OLD  24597  dvlip  24890  plymullem1  25108  lgsdir2  26211  lgsdchr  26236  brbtwn2  26996  axcontlem7  27061  frgrncvvdeqlem8  28389  nvaddsub4  28738  hhcno  29985  hhcnf  29986  unopf1o  29997  counop  30002  afsval  32363  ontopbas  34354  onsuct0  34367  heicant  35549  ftc1anclem6  35592  equivbnd2  35687  ismtybndlem  35701  ismrer1  35733  iccbnd  35735  ghomco  35786  rngohomco  35869  rngoisocnv  35876  rngoisoco  35877  idlsubcl  35918  xihopellsmN  39005  dihopellsm  39006  mhphf  39995  dvconstbi  41625  imasetpreimafvbijlemf1  44529  fargshiftf1  44566  mgmhmpropd  45012  elpglem1  46087