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 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		anim12dan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
4	3	ex 412	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
5	2, 4	anim12d 610	. 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  7285  isocnv3  7287  f1oiso2  7307  xpexr2  7870  f1o2ndf1  8072  fnwelem  8081  omword  8505  oeword  8526  swoso  8678  xpf1o  9077  zorn2lem6  10423  ltapr  10968  ltord1  11676  pc11  16851  imasaddfnlem  17492  imasaddflem  17494  pslem  18538  mgmhmpropd  18666  mhmpropd  18760  frmdsssubm  18829  ghmsub  19199  gasubg  19277  invrpropd  20398  znfld  21540  cygznlem3  21549  mplcoe5lem  22017  evlseu  22061  cpmatmcl  22684  tgclb  22935  innei  23090  txcn  23591  txflf  23971  qustgplem  24086  clmsub4  25073  cfilresi  25262  volcn  25573  itg1addlem4  25666  dvlip  25960  plymullem1  26179  lgsdir2  27293  lgsdchr  27318  brbtwn2  28974  axcontlem7  29039  frgrncvvdeqlem8  30376  nvaddsub4  30728  hhcno  31975  hhcnf  31976  unopf1o  31987  counop  31992  mndlactf1o  33090  mndractf1o  33091  afsval  34815  ontopbas  36610  onsuct0  36623  heicant  37976  ftc1anclem6  38019  equivbnd2  38113  ismtybndlem  38127  ismrer1  38159  iccbnd  38161  ghomco  38212  rngohomco  38295  rngoisocnv  38302  rngoisoco  38303  idlsubcl  38344  xihopellsmN  41700  dihopellsm  41701  f1o2d2  42674  dvconstbi  44761  ovolval5lem3  47082  imasetpreimafvbijlemf1  47858  fargshiftf1  47895  upgrimtrlslem2  48375  elpglem1  50180