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

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
StepHypRef Expression
1 syl2an2.1 . . 3 (𝜑𝜓)
21adantl 483 . 2 ((𝜒𝜑) → 𝜓)
3 syl2an2.2 . 2 ((𝜒𝜑) → 𝜃)
4 syl2an2.3 . 2 ((𝜓𝜃) → 𝜏)
52, 3, 4syl2anc 585 1 ((𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
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  3649  reusv2lem3  5360  fvmpt2d  6966  fmptco  7080  peano5  7835  peano5OLD  7836  fczsupp0  8129  suppco  8142  oeworde  8545  xpsnen2g  9016  f1domfi  9135  enfii  9140  dffi3  9374  hartogslem1  9485  ttrcltr  9659  isinffi  9935  fseqdom  9969  indcardi  9984  cfslb  10209  fin23lem31  10286  tsksdom  10699  inaprc  10779  fcdmnn0fsuppg  12479  fznatpl1  13502  fzneuz  13529  fzospliti  13611  modifeq2int  13845  hashimarn  14347  cshwsublen  14691  revco  14730  rtrclreclem3  14952  summolem2a  15607  fsum  15612  prodmolem2a  15824  fprod  15831  fzocongeq  16213  odd2np1lem  16229  divalgmod  16295  gcdcllem1  16386  eucalginv  16467  lcmfunsnlem2  16523  lcmflefac  16531  cncongr2  16551  gsumwspan  18663  orbsta  19100  efgredeu  19541  frlmbasfsupp  21180  frlmbasmap  21181  mamufacex  21754  matinvgcell  21800  2basgen  22356  ppttop  22373  ordtbaslem  22555  2ndc1stc  22818  xkopt  23022  cnflf2  23370  ngptgp  24008  xmetdcn2  24216  cncfcdm  24277  minveclem3b  24808  mbfeqalem1  25021  limcmpt  25263  ply1divex  25517  elplyd  25579  taylfval  25734  cxpeq  26126  rlimcnp  26331  muval1  26498  lgsval2lem  26671  dchrisum0flblem2  26873  dchrisum0  26884  axlowdimlem16  27948  usgr1v  28246  cplgr2vpr  28423  vtxdg0e  28464  wlknewwlksn  28874  wwlksnextwrd  28884  wwlksnwwlksnon  28902  clwlkclwwlklem2a4  28983  numclwwlk8  29378  imadifxp  31561  esum2dlem  32731  fv1stcnv  34390  bj-restsnss  35583  bj-restsnss2  35584  irrdiff  35826  domalom  35904  poimirlem16  36123  poimirlem17  36124  ftc1cnnc  36179  fnsnbt  40686  omcl2  41697  k0004lem3  42495  fvmpt2df  43575  xlimpnfxnegmnf  44129  funressnbrafv2  45550  fpprmod  45993
  Copyright terms: Public domain W3C validator