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  7259  isocnv3  7261  f1oiso2  7281  xpexr2  7844  f1o2ndf1  8047  fnwelem  8056  omword  8480  oeword  8500  swoso  8651  xpf1o  9047  zorn2lem6  10384  ltapr  10928  ltord1  11635  pc11  16784  imasaddfnlem  17424  imasaddflem  17426  pslem  18470  mgmhmpropd  18598  mhmpropd  18692  frmdsssubm  18761  ghmsub  19129  gasubg  19207  invrpropd  20329  znfld  21490  cygznlem3  21499  mplcoe5lem  21967  evlseu  22011  cpmatmcl  22627  tgclb  22878  innei  23033  txcn  23534  txflf  23914  qustgplem  24029  clmsub4  25026  cfilresi  25215  volcn  25527  itg1addlem4  25620  dvlip  25918  plymullem1  26139  lgsdir2  27261  lgsdchr  27286  brbtwn2  28876  axcontlem7  28941  frgrncvvdeqlem8  30276  nvaddsub4  30627  hhcno  31874  hhcnf  31875  unopf1o  31886  counop  31891  mndlactf1o  33001  mndractf1o  33002  afsval  34674  ontopbas  36441  onsuct0  36454  heicant  37674  ftc1anclem6  37717  equivbnd2  37811  ismtybndlem  37825  ismrer1  37857  iccbnd  37859  ghomco  37910  rngohomco  37993  rngoisocnv  38000  rngoisoco  38001  idlsubcl  38042  xihopellsmN  41272  dihopellsm  41273  f1o2d2  42245  dvconstbi  44346  ovolval5lem3  46671  imasetpreimafvbijlemf1  47414  fargshiftf1  47451  upgrimtrlslem2  47915  elpglem1  49722