Theorem anim12dan 618

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 608	. 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:  2f1fvneq  7297  isocnv  7366  isocnv3  7368  f1oiso2  7388  xpexr2  7959  f1o2ndf1  8163  fnwelem  8172  omword  8626  oeword  8646  swoso  8797  xpf1o  9205  zorn2lem6  10570  ltapr  11114  ltord1  11816  pc11  16927  imasaddfnlem  17588  imasaddflem  17590  pslem  18642  mgmhmpropd  18736  mhmpropd  18827  frmdsssubm  18896  ghmsub  19264  gasubg  19342  invrpropd  20444  znfld  21602  cygznlem3  21611  mplcoe5lem  22080  evlseu  22130  cpmatmcl  22746  tgclb  22998  innei  23154  txcn  23655  txflf  24035  qustgplem  24150  clmsub4  25158  cfilresi  25348  volcn  25660  itg1addlem4  25753  itg1addlem4OLD  25754  dvlip  26052  plymullem1  26273  lgsdir2  27392  lgsdchr  27417  brbtwn2  28938  axcontlem7  29003  frgrncvvdeqlem8  30338  nvaddsub4  30689  hhcno  31936  hhcnf  31937  unopf1o  31948  counop  31953  mndlactf1o  33016  mndractf1o  33017  afsval  34648  ontopbas  36394  onsuct0  36407  heicant  37615  ftc1anclem6  37658  equivbnd2  37752  ismtybndlem  37766  ismrer1  37798  iccbnd  37800  ghomco  37851  rngohomco  37934  rngoisocnv  37941  rngoisoco  37942  idlsubcl  37983  xihopellsmN  41211  dihopellsm  41212  f1o2d2  42228  dvconstbi  44303  ovolval5lem3  46575  imasetpreimafvbijlemf1  47278  fargshiftf1  47315  elpglem1  48803