Theorem syl2an2 684

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  elrab3t  3682  reusv2lem3  5398  fvmpt2d  7011  fmptco  7126  peano5  7883  peano5OLD  7884  fczsupp0  8177  suppco  8190  oeworde  8592  xpsnen2g  9064  f1domfi  9183  enfii  9188  dffi3  9425  hartogslem1  9536  ttrcltr  9710  isinffi  9986  fseqdom  10020  indcardi  10035  cfslb  10260  fin23lem31  10337  tsksdom  10750  inaprc  10830  fcdmnn0fsuppg  12530  fznatpl1  13554  fzneuz  13581  fzospliti  13663  modifeq2int  13897  hashimarn  14399  cshwsublen  14745  revco  14784  rtrclreclem3  15006  summolem2a  15660  fsum  15665  prodmolem2a  15877  fprod  15884  fzocongeq  16266  odd2np1lem  16282  divalgmod  16348  gcdcllem1  16439  eucalginv  16520  lcmfunsnlem2  16576  lcmflefac  16584  cncongr2  16604  gsumwspan  18726  orbsta  19176  efgredeu  19619  frlmbasfsupp  21312  frlmbasmap  21313  mamufacex  21890  matinvgcell  21936  2basgen  22492  ppttop  22509  ordtbaslem  22691  2ndc1stc  22954  xkopt  23158  cnflf2  23506  ngptgp  24144  xmetdcn2  24352  cncfcdm  24413  minveclem3b  24944  mbfeqalem1  25157  limcmpt  25399  ply1divex  25653  elplyd  25715  taylfval  25870  cxpeq  26262  rlimcnp  26467  muval1  26634  lgsval2lem  26807  dchrisum0flblem2  27009  dchrisum0  27020  cutlt  27416  axlowdimlem16  28212  usgr1v  28510  cplgr2vpr  28687  vtxdg0e  28728  wlknewwlksn  29138  wwlksnextwrd  29148  wwlksnwwlksnon  29166  clwlkclwwlklem2a4  29247  numclwwlk8  29642  imadifxp  31827  esum2dlem  33085  fv1stcnv  34743  bj-restsnss  35959  bj-restsnss2  35960  irrdiff  36202  domalom  36280  poimirlem16  36499  poimirlem17  36500  ftc1cnnc  36555  fnsnbt  41053  f1o2d2  41057  omcl2  42073  k0004lem3  42890  fvmpt2df  43967  xlimpnfxnegmnf  44520  funressnbrafv2  45942  fpprmod  46385