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  3670  reusv2lem3  5370  fvmpt2d  6999  fmptco  7119  fnsnbg  7156  peano5  7889  fczsupp0  8192  suppco  8205  oeworde  8605  xpsnen2g  9079  f1domfi  9195  enfii  9200  dffi3  9443  hartogslem1  9556  ttrcltr  9730  isinffi  10006  fseqdom  10040  indcardi  10055  cfslb  10280  fin23lem31  10357  tsksdom  10770  inaprc  10850  fcdmnn0fsuppg  12561  fznatpl1  13595  fzneuz  13625  fzospliti  13708  modifeq2int  13951  hashimarn  14458  cshwsublen  14814  revco  14853  rtrclreclem3  15079  summolem2a  15731  fsum  15736  prodmolem2a  15950  fprod  15957  fzocongeq  16343  odd2np1lem  16359  divalgmod  16425  gcdcllem1  16518  eucalginv  16603  lcmfunsnlem2  16659  lcmflefac  16667  cncongr2  16687  gsumwspan  18824  orbsta  19296  efgredeu  19733  frlmbasfsupp  21718  frlmbasmap  21719  psdmul  22104  mamufacex  22334  matinvgcell  22373  2basgen  22928  ppttop  22945  ordtbaslem  23126  2ndc1stc  23389  xkopt  23593  cnflf2  23941  ngptgp  24575  xmetdcn2  24777  cncfcdm  24842  minveclem3b  25380  mbfeqalem1  25594  limcmpt  25836  ply1divex  26094  elplyd  26159  taylfval  26318  cxpeq  26719  rlimcnp  26927  muval1  27095  lgsval2lem  27270  dchrisum0flblem2  27472  dchrisum0  27483  cutlt  27892  axlowdimlem16  28936  usgr1v  29235  cplgr2vpr  29412  vtxdg0e  29454  wlknewwlksn  29869  wwlksnextwrd  29879  wwlksnwwlksnon  29897  clwlkclwwlklem2a4  29978  numclwwlk8  30373  imadifxp  32582  esum2dlem  34123  fv1stcnv  35794  bj-restsnss  37101  bj-restsnss2  37102  irrdiff  37344  domalom  37422  poimirlem16  37660  poimirlem17  37661  ftc1cnnc  37716  f1o2d2  42284  readvrec2  42404  omcl2  43357  k0004lem3  44173  fvmpt2df  45296  xlimpnfxnegmnf  45843  funressnbrafv2  47273  fpprmod  47741  isubgriedg  47876  isubgrvtx  47880  isubgr3stgrlem2  47979  gpgusgralem  48060