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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  isocnv  7305  isocnv3  7307  f1oiso2  7327  xpexr2  7895  f1o2ndf1  8101  fnwelem  8110  omword  8534  oeword  8554  swoso  8705  xpf1o  9103  zorn2lem6  10454  ltapr  10998  ltord1  11704  pc11  16851  imasaddfnlem  17491  imasaddflem  17493  pslem  18531  mgmhmpropd  18625  mhmpropd  18719  frmdsssubm  18788  ghmsub  19156  gasubg  19234  invrpropd  20327  znfld  21470  cygznlem3  21479  mplcoe5lem  21946  evlseu  21990  cpmatmcl  22606  tgclb  22857  innei  23012  txcn  23513  txflf  23893  qustgplem  24008  clmsub4  25006  cfilresi  25195  volcn  25507  itg1addlem4  25600  dvlip  25898  plymullem1  26119  lgsdir2  27241  lgsdchr  27266  brbtwn2  28832  axcontlem7  28897  frgrncvvdeqlem8  30235  nvaddsub4  30586  hhcno  31833  hhcnf  31834  unopf1o  31845  counop  31850  mndlactf1o  32971  mndractf1o  32972  afsval  34662  ontopbas  36416  onsuct0  36429  heicant  37649  ftc1anclem6  37692  equivbnd2  37786  ismtybndlem  37800  ismrer1  37832  iccbnd  37834  ghomco  37885  rngohomco  37968  rngoisocnv  37975  rngoisoco  37976  idlsubcl  38017  xihopellsmN  41248  dihopellsm  41249  f1o2d2  42221  dvconstbi  44323  ovolval5lem3  46652  imasetpreimafvbijlemf1  47405  fargshiftf1  47442  upgrimtrlslem2  47905  elpglem1  49700