Theorem syl2an2 693

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

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  elrab3t  3630  reusv2lem3  5332  fvmpt2d  6953  fmptco  7075  fnsnbg  7112  peano5  7837  mpof1o2d  8069  fczsupp0  8137  suppco  8150  oeworde  8523  xpsnen2g  9002  f1domfi  9109  enfii  9114  dffi3  9338  hartogslem1  9451  ttrcltr  9632  isinffi  9911  fseqdom  9943  indcardi  9958  cfslb  10183  fin23lem31  10260  tsksdom  10674  inaprc  10754  fcdmnn0fsuppg  12492  fznatpl1  13527  fzneuz  13557  fzospliti  13641  modifeq2int  13890  hashimarn  14397  cshwsublen  14753  revco  14791  rtrclreclem3  15017  summolem2a  15672  fsum  15677  prodmolem2a  15894  fprod  15901  fzocongeq  16288  odd2np1lem  16304  divalgmod  16370  gcdcllem1  16463  eucalginv  16548  lcmfunsnlem2  16604  lcmflefac  16612  cncongr2  16632  gsumwspan  18809  orbsta  19283  efgredeu  19722  frlmbasfsupp  21737  frlmbasmap  21738  psdmul  22158  mamufacex  22383  matinvgcell  22422  2basgen  22977  ppttop  22994  ordtbaslem  23175  2ndc1stc  23438  xkopt  23642  cnflf2  23990  ngptgp  24623  xmetdcn2  24825  cncfcdm  24887  minveclem3b  25417  mbfeqalem1  25630  limcmpt  25872  ply1divex  26124  elplyd  26189  taylfval  26346  cxpeq  26743  rlimcnp  26951  muval1  27118  lgsval2lem  27292  dchrisum0flblem2  27494  dchrisum0  27505  cutlt  27946  axlowdimlem16  29048  usgr1v  29347  cplgr2vpr  29524  vtxdg0e  29565  wlknewwlksn  29977  wwlksnextwrd  29987  wwlksnwwlksnon  30005  clwlkclwwlklem2a4  30089  numclwwlk8  30484  imadifxp  32694  esum2dlem  34288  fv1stcnv  36020  bj-restsnss  37456  bj-restsnss2  37457  irrdiff  37701  domalom  37781  poimirlem16  38018  poimirlem17  38019  ftc1cnnc  38074  readvrec2  42853  omcl2  43793  k0004lem3  44608  fvmpt2df  45730  xlimpnfxnegmnf  46271  funressnbrafv2  47721  fpprmod  48232  isubgriedg  48368  isubgrvtx  48372  isubgr3stgrlem2  48472  gpgusgralem  48561