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

Theorem syl2anr 465
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 464 . 2  |-  ( (
ph  /\  ta )  ->  th )
54ancoms 440 1  |-  ( ( ta  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  swopo  4505  findsg  4864  coexg  5404  funco  5483  resdif  5688  fnpr  5942  fnprOLD  5943  fnsuppres  5944  isotr  6048  weisoeq  6068  xpexgALT  6289  brrpssg  6516  oaass  6796  oeword  6825  oeworde  6828  ixpssmapg  7084  pw2f1olem  7204  domsdomtr  7234  xpen  7262  mapen  7263  mapdom1  7264  elfir  7412  wdomen2  7537  carden2b  7846  harcard  7857  isinffi  7871  acnlem  7921  acndom  7924  alephdom  7954  fin23lem21  8211  fin23lem39  8222  isf32lem5  8229  fin1a2lem12  8283  ttukeylem1  8381  pwcfsdom  8450  canthp1  8521  nqereu  8798  addpqf  8813  axmulf  9013  axmulass  9024  axdistr  9025  negeu  9288  fimaxre3  9949  nnsub  10030  nn0sub  10262  elz2  10290  uzaddcl  10525  qaddcl  10582  xltneg  10795  xleneg  10796  supxrbnd1  10892  infmxrgelb  10905  iccneg  11010  fzsplit2  11068  fzss1  11083  uzsplit  11110  fzm1  11119  fzouzsplit  11160  elfznelfzob  11185  fllt  11207  uzsup  11236  om2uzlt2i  11283  nn0ennn  11310  seqfveq2  11337  sermono  11347  seqf1o  11356  ser1const  11371  faclbnd  11573  bcval4  11590  bcpasc  11604  hashkf  11612  hashunx  11652  hashfacen  11695  fz1isolem  11702  seqcoll  11704  revccat  11790  s1co  11794  shftfval  11877  seqshft  11892  crim  11912  caubnd  12154  isercolllem2  12451  fsumcvg  12498  zsum  12504  fsumcvg2  12513  fsumshftm  12556  fsumo1  12583  isumshft  12611  harmonic  12630  cvgrat  12652  mertenslem1  12653  rpnnen2  12817  dvdsval3  12848  negdvdsb  12858  dvdsnegb  12859  dvdsmul1  12863  odd2np1  12900  divalglem8  12912  ndvdsadd  12920  dvdssqim  13045  nn0seqcvgd  13053  seq1st  13054  algcvgblem  13060  pythagtriplem1  13182  pythagtriplem4  13185  pythagtriplem8  13189  pythagtriplem9  13190  pythagtriplem12  13192  pythagtriplem14  13194  pythagtriplem16  13196  pcexp  13225  pc2dvds  13244  pcz  13246  fldivp1  13258  pcfac  13260  pockthg  13266  infpnlem1  13270  prmreclem1  13276  prmreclem2  13277  1arith  13287  4sqlem11  13315  vdwlem2  13342  vdwlem8  13348  vdwnnlem2  13356  pwsval  13700  isacs1i  13874  ismgmid  14702  mhmpropd  14736  grpsubid1  14866  mulgnnp1  14890  mulgsubcl  14896  mulgnn0z  14902  mulgnndir  14904  mulgneg2  14909  lagsubg  14994  ghmco  15017  pgpfi2  15232  efgsfo  15363  frgpupf  15397  frgpup1  15399  ablfac1eu  15623  pgpfac1lem2  15625  ablfaclem3  15637  dvdsrid  15748  dvdsrneg  15751  dvr1  15786  abv1  15913  lbsexg  16228  xrsds  16733  znf1o  16824  isclo  17143  resttopon  17217  restcld  17228  restcls  17237  iscn  17291  iscnp  17293  cnco  17322  cndis  17347  cnindis  17348  cmpsub  17455  hauscmplem  17461  cmpfii  17464  ptcnplem  17645  txtube  17664  txcmplem1  17665  xkoptsub  17678  qtoptop  17724  kqfval  17747  hmeoco  17796  fileln0  17874  trfil1  17910  trfil2  17911  trufil  17934  elfm3  17974  hausflf2  18022  isucn  18300  bl2in  18422  metss2lem  18533  metss2  18534  stdbdxmet  18537  metrest  18546  nmfval2  18630  nmval2  18631  nmoix  18755  ioo2bl  18816  xrsxmet  18832  expcn  18894  elcncf  18911  icccvx  18967  iscmet3  19238  causs  19243  metcld2  19251  cmetss  19259  cncmet  19267  bcth3  19276  ovolgelb  19368  ovolfi  19382  shft2rab  19396  uniioombllem3  19469  dyadmax  19482  dyadmbl  19484  subopnmbl  19488  volcn  19490  mbfid  19520  mbfeqalem  19526  mbfres  19528  cnmbf  19543  i1fmulc  19587  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  itg2seq  19626  itg2gt0  19644  itgss3  19698  dvexp  19831  plypow  20116  plyeq0lem  20121  coeidlem  20148  dgrlt  20176  dgrcolem2  20184  elqaalem2  20229  aacjcl  20236  aaliou3lem1  20251  aaliou3lem2  20252  pserdvlem2  20336  abelthlem8  20347  cosord  20426  sinord  20428  resinf1o  20430  relogexp  20482  logdivlt  20508  advlogexp  20538  logcxp  20552  cxpcl  20557  rpcxpcl  20559  cxpne0  20560  birthdaylem2  20783  cxplim  20802  divsqrsumo1  20814  wilthlem1  20843  ftalem7  20853  basellem1  20855  sgmss  20881  issqf  20911  sqf11  20914  sgmf  20920  sgmnncl  20922  sqff1o  20957  dvdsflsumcom  20965  dvdsmulf1o  20971  sgmppw  20973  chtublem  20987  chtub  20988  logexprlim  21001  bposlem3  21062  bposlem5  21064  bposlem6  21065  lgsdirnn0  21115  lgsquad2  21136  lgsquad3  21137  dchrisumlem1  21175  dchrisumlem2  21176  dchrisumlem3  21177  mulogsumlem  21217  usgrafilem2  21418  cusgraexi  21469  cusgrafilem2  21481  hashnbgravdg  21674  nvo00  22254  nmorepnf  22261  ubthlem1  22364  normpyc  22640  occon3  22791  pjpreeq  22892  idcnop  23476  riesz3i  23557  cnlnssadj  23575  rnbra  23602  strlem3a  23747  cvcon3  23779  ssdmd1  23808  ssdmd2  23809  fzsplit3  24142  ishashinf  24151  esumcst  24447  dmvlsiga  24504  ballotlemimin  24755  zetacvg  24791  derangsn  24848  iscvm  24938  cvmsval  24945  cvmliftlem7  24970  cvmlift2lem12  24993  supfz  25191  zprod  25255  faclimlem3  25356  preduz  25467  predfz  25470  wfrlem10  25539  nobndlem2  25640  brbtwn  25830  bpolylem  26086  bpolysum  26091  bpolydiflem  26092  fsumkthpow  26094  nndivlub  26200  ltflcei  26231  lxflflp1  26233  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ftc1anclem1  26270  ftc1anclem4  26273  ftc1anclem5  26274  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  opnrebl2  26315  nn0prpwlem  26316  tailval  26393  fzadd2  26436  caushft  26458  ismtyval  26500  heiborlem7  26517  heiborlem10  26520  heibor  26521  elrfirn  26740  ismrc  26746  nacsfix  26757  mzpcompact2lem  26799  eldiophb  26806  ellz1  26816  rexrabdioph  26845  rpexpmord  27002  congrep  27029  jm2.26a  27062  lindfmm  27265  rngunsnply  27346  mendrng  27468  expgrowthi  27518  cnfex  27666  itgsinexp  27716  ltsubnn0  28082  fz0fzdiffz0  28103  ubmelm1fzo  28110  ssfzo12  28113  subsubelfzo0  28118  modifeq2int  28139  swrdltnd  28153  swrdnd  28154  swrdvalodm2  28160  swrdswrd  28165  swrdccatin12lem3  28178  swrdccat3  28181  modprm0  28194  cshwidx  28208  cshwidxmod  28209  cshwidxm1  28211  2cshw1lem1  28214  2cshw1lem2  28215  2cshw2lem2  28219  2cshw  28222  cshweqdif2  28233  cshweqrep  28237  cshw1v  28239  cshwsame  28240  cshwssizelem4a  28246  cshwssizelem4  28247  usgra2wlkspthlem2  28260  4cycl2v2nb  28343  frg2woteqm  28385  2spotmdisj  28394  bnj545  29203  bnj929  29244  bnj953  29247
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator