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  3642  reusv2lem3  5340  fvmpt2d  6948  fmptco  7068  fnsnbg  7104  peano5  7829  fczsupp0  8129  suppco  8142  oeworde  8514  xpsnen2g  8990  f1domfi  9097  enfii  9102  dffi3  9322  hartogslem1  9435  ttrcltr  9613  isinffi  9892  fseqdom  9924  indcardi  9939  cfslb  10164  fin23lem31  10241  tsksdom  10654  inaprc  10734  fcdmnn0fsuppg  12448  fznatpl1  13480  fzneuz  13510  fzospliti  13593  modifeq2int  13842  hashimarn  14349  cshwsublen  14705  revco  14743  rtrclreclem3  14969  summolem2a  15624  fsum  15629  prodmolem2a  15843  fprod  15850  fzocongeq  16237  odd2np1lem  16253  divalgmod  16319  gcdcllem1  16412  eucalginv  16497  lcmfunsnlem2  16553  lcmflefac  16561  cncongr2  16581  gsumwspan  18756  orbsta  19227  efgredeu  19666  frlmbasfsupp  21697  frlmbasmap  21698  psdmul  22082  mamufacex  22312  matinvgcell  22351  2basgen  22906  ppttop  22923  ordtbaslem  23104  2ndc1stc  23367  xkopt  23571  cnflf2  23919  ngptgp  24552  xmetdcn2  24754  cncfcdm  24819  minveclem3b  25356  mbfeqalem1  25570  limcmpt  25812  ply1divex  26070  elplyd  26135  taylfval  26294  cxpeq  26695  rlimcnp  26903  muval1  27071  lgsval2lem  27246  dchrisum0flblem2  27448  dchrisum0  27459  cutlt  27877  axlowdimlem16  28937  usgr1v  29236  cplgr2vpr  29413  vtxdg0e  29455  wlknewwlksn  29867  wwlksnextwrd  29877  wwlksnwwlksnon  29895  clwlkclwwlklem2a4  29979  numclwwlk8  30374  imadifxp  32583  esum2dlem  34126  fv1stcnv  35842  bj-restsnss  37148  bj-restsnss2  37149  irrdiff  37391  domalom  37469  poimirlem16  37696  poimirlem17  37697  ftc1cnnc  37752  f1o2d2  42351  readvrec2  42479  omcl2  43450  k0004lem3  44266  fvmpt2df  45393  xlimpnfxnegmnf  45936  funressnbrafv2  47368  fpprmod  47851  isubgriedg  47987  isubgrvtx  47991  isubgr3stgrlem2  48091  gpgusgralem  48180