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  3644  reusv2lem3  5362  fvmpt2d  6999  fmptco  7122  fnsnbg  7161  peano5  7894  mpof1o2d  8126  fczsupp0  8194  suppco  8207  oeworde  8586  xpsnen2g  9073  f1domfi  9180  enfii  9185  dffi3  9407  hartogslem1  9520  ttrcltr  9701  isinffi  10054  fseqdom  10086  indcardi  10101  cfslb  10325  fin23lem31  10402  tsksdom  10822  inaprc  10902  fcdmnn0fsuppg  12647  fznatpl1  13692  fzneuz  13722  fzospliti  13806  modifeq2int  14056  hashimarn  14565  cshwsublen  14927  revco  14965  rtrclreclem3  15193  summolem2a  15861  fsum  15866  prodmolem2a  16081  fprod  16088  fzocongeq  16474  odd2np1lem  16490  divalgmod  16556  gcdcllem1  16649  eucalginv  16739  lcmfunsnlem2  16795  lcmflefac  16803  cncongr2  16823  gsumwspan  19022  orbsta  19507  efgredeu  19946  frlmbasfsupp  22044  frlmbasmap  22045  psdmul  22467  mamufacex  22691  matinvgcell  22730  2basgen  23288  ppttop  23305  ordtbaslem  23486  2ndc1stc  23749  xkopt  23954  cnflf2  24302  ngptgp  24935  xmetdcn2  25137  cncfcdm  25199  minveclem3b  25729  mbfeqalem1  25942  limcmpt  26183  ply1divex  26435  elplyd  26500  taylfval  26668  cxpeq  27067  rlimcnp  27275  muval1  27442  lgsval2lem  27616  dchrisum0flblem2  27818  dchrisum0  27829  cutlt  28300  axlowdimlem16  29517  usgr1v  29819  cplgr2vpr  29996  vtxdg0e  30037  wlknewwlksn  30458  wwlksnextwrd  30468  wwlksnwwlksnon  30486  clwlkclwwlklem2a4  30570  numclwwlk8  30975  imadifxp  33177  esum2dlem  34706  fv1stcnv  36511  bj-restsnss  37972  bj-restsnss2  37973  irrdiff  38215  domalom  38295  poimirlem16  38522  poimirlem17  38523  ftc1cnnc  38578  dfprop1  38613  readvrec2  43380  omcl2  44293  k0004lem3  45108  fvmpt2df  46227  sumnnodd  46586  xlimpnfxnegmnf  46768  funressnbrafv2  48258  fpprmod  48769  isubgriedg  48905  isubgrvtx  48909  isubgr3stgrlem2  49009  gpgusgralem  49098