Theorem syl2an2 698

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  elrab3t  3652  reusv2lem3  5362  fvmpt2d  6993  fmptco  7115  fnsnbg  7152  peano5  7878  mpof1o2d  8109  fczsupp0  8177  suppco  8190  oeworde  8567  xpsnen2g  9046  f1domfi  9153  enfii  9158  dffi3  9379  hartogslem1  9492  ttrcltr  9673  isinffi  9966  fseqdom  9998  indcardi  10013  cfslb  10238  fin23lem31  10315  tsksdom  10729  inaprc  10809  fcdmnn0fsuppg  12555  fznatpl1  13597  fzneuz  13627  fzospliti  13711  modifeq2int  13960  hashimarn  14467  cshwsublen  14823  revco  14861  rtrclreclem3  15087  summolem2a  15756  fsum  15761  prodmolem2a  15978  fprod  15985  fzocongeq  16372  odd2np1lem  16388  divalgmod  16454  gcdcllem1  16547  eucalginv  16632  lcmfunsnlem2  16688  lcmflefac  16696  cncongr2  16716  gsumwspan  18895  orbsta  19374  efgredeu  19813  frlmbasfsupp  21868  frlmbasmap  21869  psdmul  22289  mamufacex  22514  matinvgcell  22553  2basgen  23108  ppttop  23125  ordtbaslem  23306  2ndc1stc  23569  xkopt  23773  cnflf2  24121  ngptgp  24754  xmetdcn2  24956  cncfcdm  25018  minveclem3b  25548  mbfeqalem1  25761  limcmpt  26003  ply1divex  26255  elplyd  26320  taylfval  26480  cxpeq  26880  rlimcnp  27088  muval1  27255  lgsval2lem  27429  dchrisum0flblem2  27631  dchrisum0  27642  cutlt  28083  axlowdimlem16  29216  usgr1v  29515  cplgr2vpr  29692  vtxdg0e  29733  wlknewwlksn  30145  wwlksnextwrd  30155  wwlksnwwlksnon  30173  clwlkclwwlklem2a4  30257  numclwwlk8  30652  imadifxp  32856  esum2dlem  34399  fv1stcnv  36140  bj-restsnss  37585  bj-restsnss2  37586  irrdiff  37830  domalom  37910  poimirlem16  38147  poimirlem17  38148  ftc1cnnc  38203  readvrec2  42982  omcl2  43922  k0004lem3  44737  fvmpt2df  45845  xlimpnfxnegmnf  46386  funressnbrafv2  47836  fpprmod  48347  isubgriedg  48483  isubgrvtx  48487  isubgr3stgrlem2  48587  gpgusgralem  48676