Theorem syl2an2 699

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  elrab3t  3643  reusv2lem3  5361  fvmpt2d  7007  fmptco  7130  fnsnbg  7169  peano5  7905  mpof1o2d  8139  fczsupp0  8213  suppco  8226  oeworde  8605  xpsnen2g  9092  f1domfi  9199  enfii  9204  dffi3  9426  hartogslem1  9539  ttrcltr  9720  isinffi  10076  fseqdom  10108  indcardi  10123  cfslb  10347  fin23lem31  10424  tsksdom  10844  inaprc  10924  fcdmnn0fsuppg  12669  fznatpl1  13715  fzneuz  13745  fzospliti  13829  modifeq2int  14079  hashimarn  14588  cshwsublen  14951  revco  14989  rtrclreclem3  15218  summolem2a  15886  fsum  15891  prodmolem2a  16106  fprod  16113  fzocongeq  16499  odd2np1lem  16515  divalgmod  16581  gcdcllem1  16674  eucalginv  16764  lcmfunsnlem2  16820  lcmflefac  16828  cncongr2  16848  gsumwspan  19047  orbsta  19532  efgredeu  19971  frlmbasfsupp  22069  frlmbasmap  22070  psdmul  22492  mamufacex  22716  matinvgcell  22755  2basgen  23313  ppttop  23330  ordtbaslem  23511  2ndc1stc  23774  xkopt  23979  cnflf2  24327  ngptgp  24960  xmetdcn2  25162  cncfcdm  25224  minveclem3b  25754  mbfeqalem1  25967  limcmpt  26208  ply1divex  26460  elplyd  26525  taylfval  26691  cxpeq  27090  rlimcnp  27298  muval1  27465  lgsval2lem  27639  dchrisum0flblem2  27841  dchrisum0  27852  cutlt  28323  axlowdimlem16  29540  usgr1v  29842  cplgr2vpr  30019  vtxdg0e  30060  wlknewwlksn  30481  wwlksnextwrd  30491  wwlksnwwlksnon  30509  clwlkclwwlklem2a4  30593  numclwwlk8  30998  imadifxp  33242  esum2dlem  34770  weexenwe  35812  fv1stcnv  36633  bj-restsnss  38096  bj-restsnss2  38097  irrdiff  38340  domalom  38420  poimirlem16  38647  poimirlem17  38648  ftc1cnnc  38703  dfprop1  38738  readvrec2  43505  omcl2  44428  k0004lem3  45242  fvmpt2df  46377  sumnnodd  46735  xlimpnfxnegmnf  46917  funressnbrafv2  48407  fpprmod  48918  isubgriedg  49054  isubgrvtx  49058  isubgr3stgrlem2  49158  gpgusgralem  49247