Theorem anim12dan 619

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  2f1fvneq  7255  isocnv  7323  isocnv3  7325  f1oiso2  7345  xpexr2  7906  f1o2ndf1  8104  fnwelem  8113  omword  8566  oeword  8586  swoso  8732  xpf1o  9135  zorn2lem6  10492  ltapr  11036  ltord1  11736  pc11  16809  imasaddfnlem  17470  imasaddflem  17472  pslem  18521  mhmpropd  18674  frmdsssubm  18738  ghmsub  19094  gasubg  19160  invrpropd  20224  znfld  21107  cygznlem3  21116  mplcoe5lem  21585  evlseu  21637  cpmatmcl  22212  tgclb  22464  innei  22620  txcn  23121  txflf  23501  qustgplem  23616  clmsub4  24613  cfilresi  24803  volcn  25114  itg1addlem4  25207  itg1addlem4OLD  25208  dvlip  25501  plymullem1  25719  lgsdir2  26822  lgsdchr  26847  brbtwn2  28152  axcontlem7  28217  frgrncvvdeqlem8  29548  nvaddsub4  29897  hhcno  31144  hhcnf  31145  unopf1o  31156  counop  31161  afsval  33671  ontopbas  35301  onsuct0  35314  heicant  36511  ftc1anclem6  36554  equivbnd2  36648  ismtybndlem  36662  ismrer1  36694  iccbnd  36696  ghomco  36747  rngohomco  36830  rngoisocnv  36837  rngoisoco  36838  idlsubcl  36879  xihopellsmN  40113  dihopellsm  40114  f1o2d2  41052  dvconstbi  43078  ovolval5lem3  45356  imasetpreimafvbijlemf1  46058  fargshiftf1  46095  mgmhmpropd  46541  elpglem1  47709