Theorem anim12dan 630

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  isocnv  7328  isocnv3  7330  f1oiso2  7350  xpexr2  7914  f1o2ndf1  8115  mpof1o2d  8119  fnwelem  8125  omword  8553  oeword  8574  swoso  8727  xpf1o  9125  zorn2lem6  10491  ltapr  11036  ltord1  11746  pc11  16946  imasaddfnlem  17588  imasaddflem  17590  pslem  18634  mgmhmpropd  18762  mhmpropd  18856  frmdsssubm  18926  ghmsub  19300  gasubg  19378  invrpropd  20507  znfld  21721  cygznlem3  21730  mplcoe5lem  22201  evlseu  22245  cpmatmcl  22887  tgclb  23138  innei  23293  txcn  23794  txflf  24174  qustgplem  24289  clmsub4  25276  cfilresi  25465  volcn  25776  itg1addlem4  25869  dvlip  26163  plymullem1  26382  lgsdir2  27505  lgsdchr  27530  brbtwn2  29266  axcontlem7  29331  frgrncvvdeqlem8  30668  nvaddsub4  31020  hhcno  32267  hhcnf  32268  unopf1o  32279  counop  32284  mndlactf1o  33359  mndractf1o  33360  afsval  35070  ontopbas  36967  onsuct0  36980  heicant  38334  ftc1anclem6  38377  equivbnd2  38471  ismtybndlem  38485  ismrer1  38517  iccbnd  38519  ghomco  38570  rngohomco  38653  rngoisocnv  38660  rngoisoco  38661  idlsubcl  38702  xihopellsmN  42056  dihopellsm  42057  dvconstbi  45072  ovolval5lem3  47396  imasetpreimafvbijlemf1  48181  fargshiftf1  48218  upgrimtrlslem2  48698  elpglem1  50517