Theorem syl2an2 686

Description: syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)

Hypotheses

Ref	Expression
syl2an2.1	⊢ (𝜑 → 𝜓)
syl2an2.2	⊢ ((𝜒 ∧ 𝜑) → 𝜃)
syl2an2.3	⊢ ((𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl2an2	⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl2an2

Step	Hyp	Ref	Expression
1		syl2an2.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3		syl2an2.2	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
4		syl2an2.3	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	syl2anc 584	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:  elrab3t  3693  reusv2lem3  5405  fvmpt2d  7028  fmptco  7148  peano5  7915  fczsupp0  8216  suppco  8229  oeworde  8629  xpsnen2g  9103  f1domfi  9218  enfii  9223  dffi3  9468  hartogslem1  9579  ttrcltr  9753  isinffi  10029  fseqdom  10063  indcardi  10078  cfslb  10303  fin23lem31  10380  tsksdom  10793  inaprc  10873  fcdmnn0fsuppg  12583  fznatpl1  13614  fzneuz  13644  fzospliti  13727  modifeq2int  13970  hashimarn  14475  cshwsublen  14830  revco  14869  rtrclreclem3  15095  summolem2a  15747  fsum  15752  prodmolem2a  15966  fprod  15973  fzocongeq  16357  odd2np1lem  16373  divalgmod  16439  gcdcllem1  16532  eucalginv  16617  lcmfunsnlem2  16673  lcmflefac  16681  cncongr2  16701  gsumwspan  18871  orbsta  19343  efgredeu  19784  frlmbasfsupp  21795  frlmbasmap  21796  psdmul  22187  mamufacex  22415  matinvgcell  22456  2basgen  23012  ppttop  23029  ordtbaslem  23211  2ndc1stc  23474  xkopt  23678  cnflf2  24026  ngptgp  24664  xmetdcn2  24872  cncfcdm  24937  minveclem3b  25475  mbfeqalem1  25689  limcmpt  25932  ply1divex  26190  elplyd  26255  taylfval  26414  cxpeq  26814  rlimcnp  27022  muval1  27190  lgsval2lem  27365  dchrisum0flblem2  27567  dchrisum0  27578  cutlt  27980  axlowdimlem16  28986  usgr1v  29287  cplgr2vpr  29464  vtxdg0e  29506  wlknewwlksn  29916  wwlksnextwrd  29926  wwlksnwwlksnon  29944  clwlkclwwlklem2a4  30025  numclwwlk8  30420  imadifxp  32620  esum2dlem  34072  fv1stcnv  35757  bj-restsnss  37065  bj-restsnss2  37066  irrdiff  37308  domalom  37386  poimirlem16  37622  poimirlem17  37623  ftc1cnnc  37678  fnsnbt  42249  f1o2d2  42252  readvrec2  42369  omcl2  43322  k0004lem3  44138  fvmpt2df  45217  xlimpnfxnegmnf  45769  funressnbrafv2  47193  fpprmod  47651  isubgriedg  47786  isubgrvtx  47790  isubgr3stgrlem2  47869  gpgusgralem  47945