MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anr Structured version   Unicode version

Theorem syl2anr 478
Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
Hypotheses
Ref Expression
syl2an.1  |-  ( ph  ->  ps )
syl2an.2  |-  ( ta 
->  ch )
syl2an.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
syl2anr  |-  ( ( ta  /\  ph )  ->  th )

Proof of Theorem syl2anr
StepHypRef Expression
1 syl2an.1 . . 3  |-  ( ph  ->  ps )
2 syl2an.2 . . 3  |-  ( ta 
->  ch )
3 syl2an.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
41, 2, 3syl2an 477 . 2  |-  ( (
ph  /\  ta )  ->  th )
54ancoms 453 1  |-  ( ( ta  /\  ph )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  swopo  4800  funco  5616  resdif  5826  fvcofneq  6024  fnprb  6114  fnprOLD  6115  fnsuppresOLD  6116  isotr  6217  weisoeq  6236  brrpssg  6567  findsg  6712  coexg  6736  xpexgALT  6778  fnsuppres  6929  oaass  7212  oeword  7241  oeworde  7244  ixpssmapg  7501  pw2f1olem  7623  domsdomtr  7654  xpen  7682  mapen  7683  mapdom1  7684  mapfienlem1  7866  elfir  7877  wdomen2  8006  carden2b  8351  harcard  8362  isinffi  8376  acnlem  8432  acndom  8435  alephdom  8465  fin23lem21  8722  fin23lem39  8733  isf32lem5  8740  fin1a2lem12  8794  ttukeylem1  8892  pwcfsdom  8961  canthp1  9035  nqereu  9310  addpqf  9325  axmulf  9526  axmulass  9537  axdistr  9538  negeu  9815  fimaxre3  10499  nnsub  10581  nn0sub  10853  elz2  10888  uzaddcl  11148  qaddcl  11209  xltneg  11427  xleneg  11428  supxrbnd1  11524  infmxrgelb  11537  iccneg  11652  uzsubsubfz  11718  fzsplit2  11721  fzss1  11733  uzsplit  11761  fzm1  11769  fz0fzdiffz0  11794  difelfzle  11799  difelfznle  11800  fzonlt0  11830  fzouzsplit  11842  eluzgtdifelfzo  11860  elfzodifsumelfzo  11864  ssfzo12  11887  elfznelfzob  11898  fllt  11925  flflp1  11926  uzsup  11972  modifeq2int  12031  om2uzlt2i  12044  nn0ennn  12071  suppssfz  12082  seqfveq2  12111  sermono  12121  seqf1o  12130  ser1const  12145  faclbnd  12350  bcval4  12367  bcpasc  12381  hashkf  12389  hashunx  12436  hashfacen  12485  fz1isolem  12492  seqcoll  12494  hash2prd  12500  swrdlend  12638  swrdnd  12639  swrdvalodm2  12646  swrdswrd  12667  swrdccatin12lem2  12696  swrdccat3  12699  revccat  12722  repswswrd  12738  cshwmodn  12748  cshwidxmod  12756  repswcshw  12762  2cshwid  12764  2cshwcom  12766  2cshwcshw  12775  cshwcshid  12777  cshwcsh2id  12778  s1co  12781  cshco  12784  shftfval  12885  seqshft  12900  crim  12930  caubnd  13173  isercolllem2  13470  fsumcvg  13516  fsumcvg2  13531  fsumshftm  13578  fsumo1  13608  isumshft  13633  harmonic  13652  cvgrat  13674  mertenslem1  13675  zprod  13726  rpnnen2  13941  dvdsval3  13972  negdvdsb  13982  dvdsnegb  13983  dvdsmul1  13987  odd2np1  14028  divalglem8  14040  ndvdsadd  14048  dvdssqim  14173  nn0seqcvgd  14181  seq1st  14182  algcvgblem  14188  powm2modprm  14310  modprm0  14312  modprmn0modprm0  14314  pythagtriplem1  14322  pythagtriplem4  14325  pythagtriplem8  14329  pythagtriplem9  14330  pythagtriplem12  14332  pythagtriplem14  14334  pythagtriplem16  14336  pcexp  14365  pc2dvds  14384  pcz  14386  fldivp1  14398  pcfac  14400  pockthg  14406  infpnlem1  14410  prmreclem1  14416  prmreclem2  14417  1arith  14427  4sqlem11  14455  vdwlem2  14482  vdwlem8  14488  vdwnnlem2  14496  cshwshashlem2  14563  cshwshashlem3  14564  pwsval  14865  isacs1i  15036  ismgmid  15870  mhmpropd  15951  grpsubid1  16102  mulgnnp1  16129  mulgsubcl  16135  mulgnn0z  16141  mulgnndir  16143  mulgneg2  16148  lagsubg  16242  ghmco  16265  symg2bas  16402  symgextfv  16422  pgpfi2  16605  efgsfo  16736  frgpupf  16770  frgpup1  16772  gsummptshft  16935  telgsumfzslem  16996  telgsums  17001  ablfac1eu  17103  pgpfac1lem2  17105  ablfaclem3  17117  dvdsrid  17279  dvdsrneg  17282  dvr1  17317  abv1  17461  lbsexg  17789  gsummoncoe1  18325  xrsds  18440  znf1o  18568  lindfmm  18840  matecl  18905  mavmul0g  19033  gsummatr01  19139  mp2pm2mplem4  19288  chfacfisf  19333  chfacfisfcpmat  19334  chfacfpmmulgsum2  19344  cpmadugsumlemF  19355  isclo  19566  resttopon  19640  restcld  19651  restcls  19660  iscn  19714  iscnp  19716  cnco  19745  cndis  19770  cnindis  19771  cmpsub  19878  hauscmplem  19884  cmpfii  19887  ptcnplem  20100  txtube  20119  txcmplem1  20120  xkoptsub  20133  qtoptop  20179  kqfval  20202  hmeoco  20251  fileln0  20329  trfil1  20365  trfil2  20366  trufil  20389  elfm3  20429  hausflf2  20477  isucn  20759  bl2in  20881  metss2lem  20992  metss2  20993  stdbdxmet  20996  metrest  21005  nmfval2  21089  nmval2  21090  nmoix  21214  ioo2bl  21276  xrsxmet  21292  expcn  21354  elcncf  21371  icccvx  21428  iscmet3  21710  causs  21715  metcld2  21723  cmetss  21731  cncmet  21739  bcth3  21748  ovolgelb  21869  ovolfi  21883  shft2rab  21897  uniioombllem3  21972  dyadmax  21985  dyadmbl  21987  subopnmbl  21991  volcn  21993  mbfid  22021  mbfeqalem  22027  mbfres  22029  cnmbf  22044  i1fmulc  22088  mbfi1fseqlem3  22102  mbfi1fseqlem4  22103  itg2seq  22127  itg2gt0  22145  itgss3  22199  dvexp  22334  plypow  22580  plyeq0lem  22585  coeidlem  22612  dgrlt  22641  dgrcolem2  22649  elqaalem2  22694  aacjcl  22701  aaliou3lem1  22716  aaliou3lem2  22717  pserdvlem2  22801  abelthlem8  22812  cosord  22897  sinord  22899  resinf1o  22901  relogexp  22958  logdivlt  22984  advlogexp  23014  logcxp  23028  cxpcl  23033  rpcxpcl  23035  cxpne0  23036  birthdaylem2  23260  cxplim  23279  divsqrtsumo1  23291  wilthlem1  23320  ftalem7  23330  basellem1  23332  sgmss  23358  issqf  23388  sqf11  23391  sgmf  23397  sgmnncl  23399  sqff1o  23434  dvdsflsumcom  23442  dvdsmulf1o  23448  sgmppw  23450  chtublem  23464  chtub  23465  logexprlim  23478  bposlem3  23539  bposlem5  23541  bposlem6  23542  lgsdirnn0  23592  lgsquad2  23613  lgsquad3  23614  dchrisumlem1  23652  dchrisumlem2  23653  dchrisumlem3  23654  mulogsumlem  23694  brbtwn  24180  usgrafilem2  24390  cusgraexi  24446  cusgrafilem2  24458  usgra2wlkspthlem2  24598  vfwlkniswwlkn  24684  clwlkisclwwlklem2fv2  24761  hashnbgravdg  24891  nbhashuvtx1  24893  rusgranumwlk  24935  4cycl2v2nb  24994  frg2woteqm  25037  2spotmdisj  25046  extwwlkfablem1  25052  numclwwlk8  25093  nvo00  25654  nmorepnf  25661  ubthlem1  25764  normpyc  26041  occon3  26193  pjpreeq  26294  idcnop  26878  riesz3i  26959  cnlnssadj  26977  rnbra  27004  strlem3a  27149  cvcon3  27181  ssdmd1  27210  ssdmd2  27211  relfi  27437  fzsplit3  27577  ishashinf  27584  esumcst  28049  dmvlsiga  28107  ballotlemimin  28422  zetacvg  28535  derangsn  28592  iscvm  28682  cvmsval  28689  cvmliftlem7  28714  cvmlift2lem12  28737  mclsssvlem  28900  supfz  29085  faclimlem3  29146  preduz  29256  predfz  29259  wfrlem10  29328  nobndlem2  29429  bpolylem  29786  bpolysum  29791  bpolydiflem  29792  fsumkthpow  29794  nndivlub  29899  finixpnum  30014  ltflcei  30019  mblfinlem2  30028  mblfinlem3  30029  mblfinlem4  30030  ftc1anclem1  30066  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  opnrebl2  30115  nn0prpwlem  30116  tailval  30167  fzadd2  30210  caushft  30230  ismtyval  30272  heiborlem7  30289  heiborlem10  30292  heibor  30293  impel  30479  elrfirn  30603  ismrc  30609  nacsfix  30620  mzpcompact2lem  30660  eldiophb  30666  ellz1  30676  rexrabdioph  30703  rpexpmord  30860  congrep  30887  jm2.26a  30918  rngunsnply  31098  mendring  31117  iocmbl  31156  isprm7  31168  expgrowthi  31214  cnfex  31357  icccncfext  31644  itgsinexp  31707  iblspltprt  31726  itgspltprt  31732  fourierdlem50  31893  fourierswlem  31967  zm1nn  32279  ltsubnn0  32281  subsubelfzo0  32292  mgmhmpropd  32427  2zrngamgm  32572  funcsetcestrclem9  32635  lincresunit3  32952  lincreslvec3  32953  isldepslvec2  32956  bnj545  33821  bnj929  33862  bnj953  33865  rp-isfinite5  37581
  Copyright terms: Public domain W3C validator