Theorem syl2an2 687

Description: syl2an 597 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 585	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  3634  reusv2lem3  5337  fvmpt2d  6955  fmptco  7076  fnsnbg  7112  peano5  7837  fczsupp0  8136  suppco  8149  oeworde  8522  xpsnen2g  9001  f1domfi  9108  enfii  9113  dffi3  9337  hartogslem1  9450  ttrcltr  9628  isinffi  9907  fseqdom  9939  indcardi  9954  cfslb  10179  fin23lem31  10256  tsksdom  10670  inaprc  10750  fcdmnn0fsuppg  12488  fznatpl1  13523  fzneuz  13553  fzospliti  13637  modifeq2int  13886  hashimarn  14393  cshwsublen  14749  revco  14787  rtrclreclem3  15013  summolem2a  15668  fsum  15673  prodmolem2a  15890  fprod  15897  fzocongeq  16284  odd2np1lem  16300  divalgmod  16366  gcdcllem1  16459  eucalginv  16544  lcmfunsnlem2  16600  lcmflefac  16608  cncongr2  16628  gsumwspan  18805  orbsta  19279  efgredeu  19718  frlmbasfsupp  21748  frlmbasmap  21749  psdmul  22142  mamufacex  22371  matinvgcell  22410  2basgen  22965  ppttop  22982  ordtbaslem  23163  2ndc1stc  23426  xkopt  23630  cnflf2  23978  ngptgp  24611  xmetdcn2  24813  cncfcdm  24875  minveclem3b  25405  mbfeqalem1  25618  limcmpt  25860  ply1divex  26112  elplyd  26177  taylfval  26335  cxpeq  26734  rlimcnp  26942  muval1  27110  lgsval2lem  27284  dchrisum0flblem2  27486  dchrisum0  27497  cutlt  27938  axlowdimlem16  29040  usgr1v  29339  cplgr2vpr  29516  vtxdg0e  29558  wlknewwlksn  29970  wwlksnextwrd  29980  wwlksnwwlksnon  29998  clwlkclwwlklem2a4  30082  numclwwlk8  30477  imadifxp  32686  esum2dlem  34252  fv1stcnv  35975  bj-restsnss  37411  bj-restsnss2  37412  irrdiff  37656  domalom  37734  poimirlem16  37971  poimirlem17  37972  ftc1cnnc  38027  f1o2d2  42688  readvrec2  42807  omcl2  43779  k0004lem3  44594  fvmpt2df  45719  xlimpnfxnegmnf  46260  funressnbrafv2  47704  fpprmod  48215  isubgriedg  48351  isubgrvtx  48355  isubgr3stgrlem2  48455  gpgusgralem  48544