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  7261  isocnv  7329  isocnv3  7331  f1oiso2  7351  xpexr2  7912  f1o2ndf1  8110  fnwelem  8119  omword  8572  oeword  8592  swoso  8738  xpf1o  9141  zorn2lem6  10498  ltapr  11042  ltord1  11742  pc11  16815  imasaddfnlem  17476  imasaddflem  17478  pslem  18527  mhmpropd  18680  frmdsssubm  18744  ghmsub  19102  gasubg  19168  invrpropd  20236  znfld  21122  cygznlem3  21131  mplcoe5lem  21600  evlseu  21652  cpmatmcl  22228  tgclb  22480  innei  22636  txcn  23137  txflf  23517  qustgplem  23632  clmsub4  24629  cfilresi  24819  volcn  25130  itg1addlem4  25223  itg1addlem4OLD  25224  dvlip  25517  plymullem1  25735  lgsdir2  26840  lgsdchr  26865  brbtwn2  28201  axcontlem7  28266  frgrncvvdeqlem8  29597  nvaddsub4  29948  hhcno  31195  hhcnf  31196  unopf1o  31207  counop  31212  afsval  33752  ontopbas  35399  onsuct0  35412  heicant  36609  ftc1anclem6  36652  equivbnd2  36746  ismtybndlem  36760  ismrer1  36792  iccbnd  36794  ghomco  36845  rngohomco  36928  rngoisocnv  36935  rngoisoco  36936  idlsubcl  36977  xihopellsmN  40211  dihopellsm  40212  f1o2d2  41141  dvconstbi  43175  ovolval5lem3  45449  imasetpreimafvbijlemf1  46151  fargshiftf1  46188  mgmhmpropd  46634  elpglem1  47834