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  7278  isocnv3  7280  f1oiso2  7300  xpexr2  7863  f1o2ndf1  8066  fnwelem  8075  omword  8499  oeword  8520  swoso  8672  xpf1o  9071  zorn2lem6  10415  ltapr  10960  ltord1  11667  pc11  16812  imasaddfnlem  17453  imasaddflem  17455  pslem  18499  mgmhmpropd  18627  mhmpropd  18721  frmdsssubm  18790  ghmsub  19157  gasubg  19235  invrpropd  20358  znfld  21519  cygznlem3  21528  mplcoe5lem  21998  evlseu  22042  cpmatmcl  22667  tgclb  22918  innei  23073  txcn  23574  txflf  23954  qustgplem  24069  clmsub4  25066  cfilresi  25255  volcn  25567  itg1addlem4  25660  dvlip  25958  plymullem1  26179  lgsdir2  27301  lgsdchr  27326  brbtwn2  28961  axcontlem7  29026  frgrncvvdeqlem8  30364  nvaddsub4  30715  hhcno  31962  hhcnf  31963  unopf1o  31974  counop  31979  mndlactf1o  33093  mndractf1o  33094  afsval  34809  ontopbas  36603  onsuct0  36616  heicant  37827  ftc1anclem6  37870  equivbnd2  37964  ismtybndlem  37978  ismrer1  38010  iccbnd  38012  ghomco  38063  rngohomco  38146  rngoisocnv  38153  rngoisoco  38154  idlsubcl  38195  xihopellsmN  41551  dihopellsm  41552  f1o2d2  42526  dvconstbi  44611  ovolval5lem3  46934  imasetpreimafvbijlemf1  47686  fargshiftf1  47723  upgrimtrlslem2  48187  elpglem1  49992