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  7286  isocnv3  7288  f1oiso2  7308  xpexr2  7871  f1o2ndf1  8074  fnwelem  8083  omword  8507  oeword  8528  swoso  8680  xpf1o  9079  zorn2lem6  10423  ltapr  10968  ltord1  11675  pc11  16820  imasaddfnlem  17461  imasaddflem  17463  pslem  18507  mgmhmpropd  18635  mhmpropd  18729  frmdsssubm  18798  ghmsub  19165  gasubg  19243  invrpropd  20366  znfld  21527  cygznlem3  21536  mplcoe5lem  22006  evlseu  22050  cpmatmcl  22675  tgclb  22926  innei  23081  txcn  23582  txflf  23962  qustgplem  24077  clmsub4  25074  cfilresi  25263  volcn  25575  itg1addlem4  25668  dvlip  25966  plymullem1  26187  lgsdir2  27309  lgsdchr  27334  brbtwn2  28990  axcontlem7  29055  frgrncvvdeqlem8  30393  nvaddsub4  30744  hhcno  31991  hhcnf  31992  unopf1o  32003  counop  32008  mndlactf1o  33122  mndractf1o  33123  afsval  34848  ontopbas  36641  onsuct0  36654  heicant  37895  ftc1anclem6  37938  equivbnd2  38032  ismtybndlem  38046  ismrer1  38078  iccbnd  38080  ghomco  38131  rngohomco  38214  rngoisocnv  38221  rngoisoco  38222  idlsubcl  38263  xihopellsmN  41619  dihopellsm  41620  f1o2d2  42594  dvconstbi  44679  ovolval5lem3  47001  imasetpreimafvbijlemf1  47753  fargshiftf1  47790  upgrimtrlslem2  48254  elpglem1  50059