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  3661  reusv2lem3  5358  fvmpt2d  6984  fmptco  7104  fnsnbg  7141  peano5  7872  fczsupp0  8175  suppco  8188  oeworde  8560  xpsnen2g  9039  f1domfi  9151  enfii  9156  dffi3  9389  hartogslem1  9502  ttrcltr  9676  isinffi  9952  fseqdom  9986  indcardi  10001  cfslb  10226  fin23lem31  10303  tsksdom  10716  inaprc  10796  fcdmnn0fsuppg  12509  fznatpl1  13546  fzneuz  13576  fzospliti  13659  modifeq2int  13905  hashimarn  14412  cshwsublen  14768  revco  14807  rtrclreclem3  15033  summolem2a  15688  fsum  15693  prodmolem2a  15907  fprod  15914  fzocongeq  16301  odd2np1lem  16317  divalgmod  16383  gcdcllem1  16476  eucalginv  16561  lcmfunsnlem2  16617  lcmflefac  16625  cncongr2  16645  gsumwspan  18780  orbsta  19252  efgredeu  19689  frlmbasfsupp  21674  frlmbasmap  21675  psdmul  22060  mamufacex  22290  matinvgcell  22329  2basgen  22884  ppttop  22901  ordtbaslem  23082  2ndc1stc  23345  xkopt  23549  cnflf2  23897  ngptgp  24531  xmetdcn2  24733  cncfcdm  24798  minveclem3b  25335  mbfeqalem1  25549  limcmpt  25791  ply1divex  26049  elplyd  26114  taylfval  26273  cxpeq  26674  rlimcnp  26882  muval1  27050  lgsval2lem  27225  dchrisum0flblem2  27427  dchrisum0  27438  cutlt  27847  axlowdimlem16  28891  usgr1v  29190  cplgr2vpr  29367  vtxdg0e  29409  wlknewwlksn  29824  wwlksnextwrd  29834  wwlksnwwlksnon  29852  clwlkclwwlklem2a4  29933  numclwwlk8  30328  imadifxp  32537  esum2dlem  34089  fv1stcnv  35771  bj-restsnss  37078  bj-restsnss2  37079  irrdiff  37321  domalom  37399  poimirlem16  37637  poimirlem17  37638  ftc1cnnc  37693  f1o2d2  42228  readvrec2  42356  omcl2  43329  k0004lem3  44145  fvmpt2df  45273  xlimpnfxnegmnf  45819  funressnbrafv2  47249  fpprmod  47732  isubgriedg  47867  isubgrvtx  47871  isubgr3stgrlem2  47970  gpgusgralem  48051