Theorem syl2an2 683

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 482	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3		syl2an2.2	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
4		syl2an2.3	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	syl2anc 584	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  elrab3t  3624  reusv2lem3  5324  fvmpt2d  6897  fmptco  7010  peano5  7749  peano5OLD  7750  fczsupp0  8018  suppco  8031  oeworde  8433  xpsnen2g  8861  f1domfi  8976  enfii  8981  dffi3  9199  hartogslem1  9310  ttrcltr  9483  isinffi  9759  fseqdom  9791  indcardi  9806  cfslb  10031  fin23lem31  10108  tsksdom  10521  inaprc  10601  frnnn0fsuppg  12301  fznatpl1  13319  fzneuz  13346  fzospliti  13428  modifeq2int  13662  hashimarn  14164  cshwsublen  14518  revco  14556  rtrclreclem3  14780  summolem2a  15436  fsum  15441  prodmolem2a  15653  fprod  15660  fzocongeq  16042  odd2np1lem  16058  divalgmod  16124  gcdcllem1  16215  eucalginv  16298  lcmfunsnlem2  16354  lcmflefac  16362  cncongr2  16382  gsumwspan  18494  orbsta  18928  efgredeu  19367  frlmbasfsupp  20974  frlmbasmap  20975  mamufacex  21547  matinvgcell  21593  2basgen  22149  ppttop  22166  ordtbaslem  22348  2ndc1stc  22611  xkopt  22815  cnflf2  23163  ngptgp  23801  xmetdcn2  24009  cncffvrn  24070  minveclem3b  24601  mbfeqalem1  24814  limcmpt  25056  ply1divex  25310  elplyd  25372  taylfval  25527  cxpeq  25919  rlimcnp  26124  muval1  26291  lgsval2lem  26464  dchrisum0flblem2  26666  dchrisum0  26677  axlowdimlem16  27334  usgr1v  27632  cplgr2vpr  27809  vtxdg0e  27850  wlknewwlksn  28261  wwlksnextwrd  28271  wwlksnwwlksnon  28289  clwlkclwwlklem2a4  28370  numclwwlk8  28765  imadifxp  30949  esum2dlem  32069  fv1stcnv  33760  bj-restsnss  35263  bj-restsnss2  35264  irrdiff  35506  domalom  35584  poimirlem16  35802  poimirlem17  35803  ftc1cnnc  35858  fnsnbt  40215  k0004lem3  41766  xlimpnfxnegmnf  43362  funressnbrafv2  44747  fpprmod  45190