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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  2f1fvneq  7165  isocnv  7233  isocnv3  7235  f1oiso2  7255  xpexr2  7798  f1o2ndf1  7994  fnwelem  8003  omword  8432  oeword  8452  swoso  8562  xpf1o  8964  zorn2lem6  10303  ltapr  10847  ltord1  11547  pc11  16626  imasaddfnlem  17284  imasaddflem  17286  pslem  18335  mhmpropd  18481  frmdsssubm  18545  ghmsub  18887  gasubg  18953  invrpropd  19985  znfld  20813  cygznlem3  20822  mplcoe5lem  21285  evlseu  21338  cpmatmcl  21913  tgclb  22165  innei  22321  txcn  22822  txflf  23202  qustgplem  23317  clmsub4  24314  cfilresi  24504  volcn  24815  itg1addlem4  24908  itg1addlem4OLD  24909  dvlip  25202  plymullem1  25420  lgsdir2  26523  lgsdchr  26548  brbtwn2  27318  axcontlem7  27383  frgrncvvdeqlem8  28715  nvaddsub4  29064  hhcno  30311  hhcnf  30312  unopf1o  30323  counop  30328  afsval  32696  ontopbas  34662  onsuct0  34675  heicant  35856  ftc1anclem6  35899  equivbnd2  35994  ismtybndlem  36008  ismrer1  36040  iccbnd  36042  ghomco  36093  rngohomco  36176  rngoisocnv  36183  rngoisoco  36184  idlsubcl  36225  xihopellsmN  39310  dihopellsm  39311  mhphf  40322  dvconstbi  41990  ovolval5lem3  44242  imasetpreimafvbijlemf1  44914  fargshiftf1  44951  mgmhmpropd  45397  elpglem1  46474