Theorem syl2an2 687

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  elrab3t  3647  reusv2lem3  5347  fvmpt2d  6963  fmptco  7084  fnsnbg  7120  peano5  7845  fczsupp0  8145  suppco  8158  oeworde  8531  xpsnen2g  9010  f1domfi  9117  enfii  9122  dffi3  9346  hartogslem1  9459  ttrcltr  9637  isinffi  9916  fseqdom  9948  indcardi  9963  cfslb  10188  fin23lem31  10265  tsksdom  10679  inaprc  10759  fcdmnn0fsuppg  12473  fznatpl1  13506  fzneuz  13536  fzospliti  13619  modifeq2int  13868  hashimarn  14375  cshwsublen  14731  revco  14769  rtrclreclem3  14995  summolem2a  15650  fsum  15655  prodmolem2a  15869  fprod  15876  fzocongeq  16263  odd2np1lem  16279  divalgmod  16345  gcdcllem1  16438  eucalginv  16523  lcmfunsnlem2  16579  lcmflefac  16587  cncongr2  16607  gsumwspan  18783  orbsta  19254  efgredeu  19693  frlmbasfsupp  21725  frlmbasmap  21726  psdmul  22121  mamufacex  22352  matinvgcell  22391  2basgen  22946  ppttop  22963  ordtbaslem  23144  2ndc1stc  23407  xkopt  23611  cnflf2  23959  ngptgp  24592  xmetdcn2  24794  cncfcdm  24859  minveclem3b  25396  mbfeqalem1  25610  limcmpt  25852  ply1divex  26110  elplyd  26175  taylfval  26334  cxpeq  26735  rlimcnp  26943  muval1  27111  lgsval2lem  27286  dchrisum0flblem2  27488  dchrisum0  27499  cutlt  27940  axlowdimlem16  29042  usgr1v  29341  cplgr2vpr  29518  vtxdg0e  29560  wlknewwlksn  29972  wwlksnextwrd  29982  wwlksnwwlksnon  30000  clwlkclwwlklem2a4  30084  numclwwlk8  30479  imadifxp  32687  esum2dlem  34269  fv1stcnv  35990  bj-restsnss  37330  bj-restsnss2  37331  irrdiff  37575  domalom  37653  poimirlem16  37881  poimirlem17  37882  ftc1cnnc  37937  f1o2d2  42599  readvrec2  42725  omcl2  43684  k0004lem3  44499  fvmpt2df  45624  xlimpnfxnegmnf  46166  funressnbrafv2  47598  fpprmod  48081  isubgriedg  48217  isubgrvtx  48221  isubgr3stgrlem2  48321  gpgusgralem  48410