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  3647  reusv2lem3  5366  fvmpt2d  7030  fmptco  7154  fnsnbg  7193  peano5  7929  mpof1o2d  8164  fczsupp0  8238  suppco  8251  oeworde  8630  xpsnen2g  9117  f1domfi  9224  enfii  9229  dffi3  9450  hartogslem1  9563  ttrcltr  9744  isinffi  10100  fseqdom  10132  indcardi  10147  cfslb  10371  fin23lem31  10448  tsksdom  10868  inaprc  10948  fcdmnn0fsuppg  12693  fznatpl1  13739  fzneuz  13769  fzospliti  13853  modifeq2int  14103  hashimarn  14612  cshwsublen  14975  revco  15013  rtrclreclem3  15242  summolem2a  15910  fsum  15915  prodmolem2a  16130  fprod  16137  fzocongeq  16523  odd2np1lem  16539  divalgmod  16605  gcdcllem1  16698  eucalginv  16788  lcmfunsnlem2  16844  lcmflefac  16852  cncongr2  16872  gsumwspan  19071  orbsta  19557  efgredeu  19996  frlmbasfsupp  22094  frlmbasmap  22095  psdmul  22517  mamufacex  22741  matinvgcell  22780  2basgen  23338  ppttop  23355  ordtbaslem  23536  2ndc1stc  23799  xkopt  24004  cnflf2  24352  ngptgp  24985  xmetdcn2  25187  cncfcdm  25249  minveclem3b  25779  mbfeqalem1  25992  limcmpt  26233  ply1divex  26485  elplyd  26550  taylfval  26716  cxpeq  27115  rlimcnp  27323  muval1  27490  lgsval2lem  27664  dchrisum0flblem2  27866  dchrisum0  27877  cutlt  28348  axlowdimlem16  29565  usgr1v  29867  cplgr2vpr  30044  vtxdg0e  30085  wlknewwlksn  30506  wwlksnextwrd  30516  wwlksnwwlksnon  30534  clwlkclwwlklem2a4  30618  numclwwlk8  31023  imadifxp  33267  esum2dlem  34794  weexenwe  35848  elpssmo  36636  fv1stcnv  36719  bj-restsnss  38195  bj-restsnss2  38196  irrdiff  38439  domalom  38519  poimirlem16  38746  poimirlem17  38747  ftc1cnnc  38802  dfprop1  38837  readvrec2  43605  omcl2  44527  k0004lem3  45341  fvmpt2df  46489  sumnnodd  46847  xlimpnfxnegmnf  47029  funressnbrafv2  48519  fpprmod  49030  isubgriedg  49166  isubgrvtx  49170  isubgr3stgrlem2  49270  gpgusgralem  49359