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  3652  reusv2lem3  5376  fvmpt2d  7010  fmptco  7132  fnsnbg  7169  peano5  7899  mpof1o2d  8130  fczsupp0  8198  suppco  8211  oeworde  8588  xpsnen2g  9068  f1domfi  9175  enfii  9180  dffi3  9401  hartogslem1  9514  ttrcltr  9695  isinffi  9997  fseqdom  10029  indcardi  10044  cfslb  10268  fin23lem31  10345  tsksdom  10759  inaprc  10839  fcdmnn0fsuppg  12582  fznatpl1  13625  fzneuz  13655  fzospliti  13739  modifeq2int  13989  hashimarn  14497  cshwsublen  14859  revco  14897  rtrclreclem3  15123  summolem2a  15792  fsum  15797  prodmolem2a  16014  fprod  16021  fzocongeq  16407  odd2np1lem  16423  divalgmod  16489  gcdcllem1  16582  eucalginv  16667  lcmfunsnlem2  16723  lcmflefac  16731  cncongr2  16751  gsumwspan  18936  orbsta  19414  efgredeu  19853  frlmbasfsupp  21945  frlmbasmap  21946  psdmul  22366  mamufacex  22590  matinvgcell  22629  2basgen  23184  ppttop  23201  ordtbaslem  23382  2ndc1stc  23645  xkopt  23849  cnflf2  24197  ngptgp  24830  xmetdcn2  25032  cncfcdm  25094  minveclem3b  25624  mbfeqalem1  25837  limcmpt  26079  ply1divex  26331  elplyd  26396  taylfval  26559  cxpeq  26959  rlimcnp  27167  muval1  27334  lgsval2lem  27508  dchrisum0flblem2  27710  dchrisum0  27721  cutlt  28162  axlowdimlem16  29344  usgr1v  29643  cplgr2vpr  29820  vtxdg0e  29861  wlknewwlksn  30273  wwlksnextwrd  30283  wwlksnwwlksnon  30301  clwlkclwwlklem2a4  30385  numclwwlk8  30780  imadifxp  32983  esum2dlem  34513  fv1stcnv  36290  bj-restsnss  37766  bj-restsnss2  37767  irrdiff  38011  domalom  38091  poimirlem16  38328  poimirlem17  38329  ftc1cnnc  38384  readvrec2  43163  omcl2  44101  k0004lem3  44916  fvmpt2df  46028  xlimpnfxnegmnf  46569  funressnbrafv2  48022  fpprmod  48533  isubgriedg  48669  isubgrvtx  48673  isubgr3stgrlem2  48773  gpgusgralem  48862