Theorem syl2an2 684

Description: syl2an 594 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 480	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3		syl2an2.2	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
4		syl2an2.3	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	syl2anc 582	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  elrab3t  3679  reusv2lem3  5394  fvmpt2d  7011  fmptco  7132  peano5  7894  peano5OLD  7895  fczsupp0  8196  suppco  8210  oeworde  8612  xpsnen2g  9092  f1domfi  9208  enfii  9213  dffi3  9464  hartogslem1  9575  ttrcltr  9749  isinffi  10025  fseqdom  10059  indcardi  10074  cfslb  10297  fin23lem31  10374  tsksdom  10787  inaprc  10867  fcdmnn0fsuppg  12574  fznatpl1  13600  fzneuz  13627  fzospliti  13709  modifeq2int  13944  hashimarn  14449  cshwsublen  14796  revco  14835  rtrclreclem3  15057  summolem2a  15711  fsum  15716  prodmolem2a  15928  fprod  15935  fzocongeq  16318  odd2np1lem  16334  divalgmod  16400  gcdcllem1  16491  eucalginv  16577  lcmfunsnlem2  16633  lcmflefac  16641  cncongr2  16661  gsumwspan  18828  orbsta  19300  efgredeu  19743  frlmbasfsupp  21749  frlmbasmap  21750  psdmul  22153  mamufacex  22381  matinvgcell  22422  2basgen  22978  ppttop  22995  ordtbaslem  23177  2ndc1stc  23440  xkopt  23644  cnflf2  23992  ngptgp  24630  xmetdcn2  24838  cncfcdm  24903  minveclem3b  25441  mbfeqalem1  25655  limcmpt  25897  ply1divex  26158  elplyd  26223  taylfval  26380  cxpeq  26779  rlimcnp  26987  muval1  27155  lgsval2lem  27330  dchrisum0flblem2  27532  dchrisum0  27543  cutlt  27943  axlowdimlem16  28885  usgr1v  29186  cplgr2vpr  29363  vtxdg0e  29405  wlknewwlksn  29815  wwlksnextwrd  29825  wwlksnwwlksnon  29843  clwlkclwwlklem2a4  29924  numclwwlk8  30319  imadifxp  32518  esum2dlem  33935  fv1stcnv  35610  bj-restsnss  36800  bj-restsnss2  36801  irrdiff  37043  domalom  37121  poimirlem16  37347  poimirlem17  37348  ftc1cnnc  37403  fnsnbt  41973  f1o2d2  41976  omcl2  43033  k0004lem3  43850  fvmpt2df  44915  xlimpnfxnegmnf  45468  funressnbrafv2  46890  fpprmod  47332  isubgriedg  47463  isubgrvtx  47465