Theorem anim12dan 631

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

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

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 402

This theorem is used by:  isocnv  7338  isocnv3  7340  f1oiso2  7360  xpexr2  7931  f1o2ndf1  8133  mpof1o2d  8137  fnwelem  8143  omword  8578  oeword  8599  swoso  8752  xpf1o  9158  zorn2lem6  10579  ltapr  11130  ltord1  11842  pc11  17058  imasaddfnlem  17700  imasaddflem  17702  pslem  18746  mgmhmpropd  18887  mhmpropd  18987  frmdsssubm  19057  ghmsub  19438  gasubg  19516  invrpropd  20648  znfld  21866  cygznlem3  21875  mplcoe5lem  22348  evlseu  22392  cpmatmcl  23037  tgclb  23288  innei  23443  txcn  23945  txflf  24325  qustgplem  24440  clmsub4  25427  cfilresi  25616  volcn  25927  itg1addlem4  26020  dvlip  26313  plymullem1  26533  lgsdir2  27657  lgsdchr  27682  brbtwn2  29483  axcontlem7  29548  frgrncvvdeqlem8  30907  nvaddsub4  31259  hhcno  32506  hhcnf  32507  unopf1o  32518  counop  32523  mndlactf1o  33591  mndractf1o  33592  afsval  35303  ontopbas  37216  onsuct0  37229  heicant  38574  ftc1anclem6  38617  equivbnd2  38727  ismtybndlem  38741  ismrer1  38773  iccbnd  38775  ghomco  38826  rngohomco  38909  rngoisocnv  38916  rngoisoco  38917  idlsubcl  38958  xihopellsmN  42312  dihopellsm  42313  dvconstbi  45318  ovolval5lem3  47664  imasetpreimafvbijlemf1  48486  fargshiftf1  48523  upgrimtrlslem2  49003  elpglem1  50804