MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2an2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 syl2an2.1 . . 3 (𝜑𝜓)
21adantl 482 . 2 ((𝜒𝜑) → 𝜓)
3 syl2an2.2 . 2 ((𝜒𝜑) → 𝜃)
4 syl2an2.3 . 2 ((𝜓𝜃) → 𝜏)
52, 3, 4syl2anc 584 1 ((𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
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  3642  reusv2lem3  5353  fvmpt2d  6958  fmptco  7071  peano5  7822  peano5OLD  7823  fczsupp0  8116  suppco  8129  oeworde  8532  xpsnen2g  8967  f1domfi  9086  enfii  9091  dffi3  9325  hartogslem1  9436  ttrcltr  9610  isinffi  9886  fseqdom  9920  indcardi  9935  cfslb  10160  fin23lem31  10237  tsksdom  10650  inaprc  10730  fcdmnn0fsuppg  12430  fznatpl1  13449  fzneuz  13476  fzospliti  13558  modifeq2int  13792  hashimarn  14294  cshwsublen  14642  revco  14681  rtrclreclem3  14905  summolem2a  15560  fsum  15565  prodmolem2a  15777  fprod  15784  fzocongeq  16166  odd2np1lem  16182  divalgmod  16248  gcdcllem1  16339  eucalginv  16420  lcmfunsnlem2  16476  lcmflefac  16484  cncongr2  16504  gsumwspan  18616  orbsta  19052  efgredeu  19493  frlmbasfsupp  21117  frlmbasmap  21118  mamufacex  21690  matinvgcell  21736  2basgen  22292  ppttop  22309  ordtbaslem  22491  2ndc1stc  22754  xkopt  22958  cnflf2  23306  ngptgp  23944  xmetdcn2  24152  cncfcdm  24213  minveclem3b  24744  mbfeqalem1  24957  limcmpt  25199  ply1divex  25453  elplyd  25515  taylfval  25670  cxpeq  26062  rlimcnp  26267  muval1  26434  lgsval2lem  26607  dchrisum0flblem2  26809  dchrisum0  26820  axlowdimlem16  27735  usgr1v  28033  cplgr2vpr  28210  vtxdg0e  28251  wlknewwlksn  28661  wwlksnextwrd  28671  wwlksnwwlksnon  28689  clwlkclwwlklem2a4  28770  numclwwlk8  29165  imadifxp  31348  esum2dlem  32503  fv1stcnv  34167  bj-restsnss  35492  bj-restsnss2  35493  irrdiff  35735  domalom  35813  poimirlem16  36032  poimirlem17  36033  ftc1cnnc  36088  fnsnbt  40593  omcl2  41573  k0004lem3  42332  fvmpt2df  43407  xlimpnfxnegmnf  43956  funressnbrafv2  45377  fpprmod  45820
  Copyright terms: Public domain W3C validator