Theorem syl2an2 685

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  elrab3t  3683  reusv2lem3  5399  fvmpt2d  7012  fmptco  7127  peano5  7884  peano5OLD  7885  fczsupp0  8178  suppco  8191  oeworde  8593  xpsnen2g  9065  f1domfi  9184  enfii  9189  dffi3  9426  hartogslem1  9537  ttrcltr  9711  isinffi  9987  fseqdom  10021  indcardi  10036  cfslb  10261  fin23lem31  10338  tsksdom  10751  inaprc  10831  fcdmnn0fsuppg  12531  fznatpl1  13555  fzneuz  13582  fzospliti  13664  modifeq2int  13898  hashimarn  14400  cshwsublen  14746  revco  14785  rtrclreclem3  15007  summolem2a  15661  fsum  15666  prodmolem2a  15878  fprod  15885  fzocongeq  16267  odd2np1lem  16283  divalgmod  16349  gcdcllem1  16440  eucalginv  16521  lcmfunsnlem2  16577  lcmflefac  16585  cncongr2  16605  gsumwspan  18727  orbsta  19177  efgredeu  19620  frlmbasfsupp  21313  frlmbasmap  21314  mamufacex  21891  matinvgcell  21937  2basgen  22493  ppttop  22510  ordtbaslem  22692  2ndc1stc  22955  xkopt  23159  cnflf2  23507  ngptgp  24145  xmetdcn2  24353  cncfcdm  24414  minveclem3b  24945  mbfeqalem1  25158  limcmpt  25400  ply1divex  25654  elplyd  25716  taylfval  25871  cxpeq  26265  rlimcnp  26470  muval1  26637  lgsval2lem  26810  dchrisum0flblem2  27012  dchrisum0  27023  cutlt  27421  axlowdimlem16  28246  usgr1v  28544  cplgr2vpr  28721  vtxdg0e  28762  wlknewwlksn  29172  wwlksnextwrd  29182  wwlksnwwlksnon  29200  clwlkclwwlklem2a4  29281  numclwwlk8  29676  imadifxp  31863  esum2dlem  33121  fv1stcnv  34779  bj-restsnss  36012  bj-restsnss2  36013  irrdiff  36255  domalom  36333  poimirlem16  36552  poimirlem17  36553  ftc1cnnc  36608  fnsnbt  41099  f1o2d2  41103  omcl2  42131  k0004lem3  42948  fvmpt2df  44025  xlimpnfxnegmnf  44578  funressnbrafv2  46000  fpprmod  46443