MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anr 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  4454  findsg  4812  coexg  5352  funco  5431  resdif  5636  fnpr  5889  fnprOLD  5890  fnsuppres  5891  isotr  5995  weisoeq  6015  xpexgALT  6236  brrpssg  6460  oaass  6740  oeword  6769  oeworde  6772  ixpssmapg  7028  pw2f1olem  7148  domsdomtr  7178  xpen  7206  mapen  7207  mapdom1  7208  elfir  7355  wdomen2  7478  carden2b  7787  harcard  7798  isinffi  7812  acnlem  7862  acndom  7865  alephdom  7895  fin23lem21  8152  fin23lem39  8163  isf32lem5  8170  fin1a2lem12  8224  ttukeylem1  8322  pwcfsdom  8391  canthp1  8462  nqereu  8739  addpqf  8754  axmulf  8954  axmulass  8965  axdistr  8966  negeu  9228  fimaxre3  9889  nnsub  9970  nn0sub  10202  elz2  10230  uzaddcl  10465  qaddcl  10522  xltneg  10735  xleneg  10736  supxrbnd1  10832  infmxrgelb  10845  iccneg  10950  fzsplit2  11008  fzss1  11023  uzsplit  11048  fzm1  11057  fzouzsplit  11098  elfznelfzob  11120  fllt  11142  uzsup  11171  om2uzlt2i  11218  nn0ennn  11245  seqfveq2  11272  sermono  11282  seqf1o  11291  ser1const  11306  faclbnd  11508  bcval4  11525  bcpasc  11539  hashkf  11547  hashunx  11587  hashfacen  11630  fz1isolem  11637  seqcoll  11639  revccat  11725  s1co  11729  shftfval  11812  seqshft  11827  crim  11847  caubnd  12089  isercolllem2  12386  fsumcvg  12433  zsum  12439  fsumcvg2  12448  fsumshftm  12491  fsumo1  12518  isumshft  12546  harmonic  12565  cvgrat  12587  mertenslem1  12588  rpnnen2  12752  dvdsval3  12783  negdvdsb  12793  dvdsnegb  12794  dvdsmul1  12798  odd2np1  12835  divalglem8  12847  ndvdsadd  12855  dvdssqim  12980  nn0seqcvgd  12988  seq1st  12989  algcvgblem  12995  pythagtriplem1  13117  pythagtriplem4  13120  pythagtriplem8  13124  pythagtriplem9  13125  pythagtriplem12  13127  pythagtriplem14  13129  pythagtriplem16  13131  pcexp  13160  pc2dvds  13179  pcz  13181  fldivp1  13193  pcfac  13195  pockthg  13201  infpnlem1  13205  prmreclem1  13211  prmreclem2  13212  1arith  13222  4sqlem11  13250  vdwlem2  13277  vdwlem8  13283  vdwnnlem2  13291  pwsval  13635  isacs1i  13809  ismgmid  14637  mhmpropd  14671  grpsubid1  14801  mulgnnp1  14825  mulgsubcl  14831  mulgnn0z  14837  mulgnndir  14839  mulgneg2  14844  lagsubg  14929  ghmco  14952  pgpfi2  15167  efgsfo  15298  frgpupf  15332  frgpup1  15334  ablfac1eu  15558  pgpfac1lem2  15560  ablfaclem3  15572  dvdsrid  15683  dvdsrneg  15686  dvr1  15721  abv1  15848  lbsexg  16163  xrsds  16664  znf1o  16755  isclo  17074  resttopon  17147  restcld  17158  restcls  17167  iscn  17221  iscnp  17223  cnco  17252  cndis  17277  cnindis  17278  cmpsub  17385  hauscmplem  17391  cmpfii  17394  ptcnplem  17574  txtube  17593  txcmplem1  17594  xkoptsub  17607  qtoptop  17653  kqfval  17676  hmeoco  17725  fileln0  17803  trfil1  17839  trfil2  17840  trufil  17863  elfm3  17903  hausflf2  17951  isucn  18229  bl2in  18331  metss2lem  18431  metss2  18432  stdbdxmet  18435  metrest  18444  nmfval2  18509  nmval2  18510  nmoix  18634  ioo2bl  18695  xrsxmet  18711  expcn  18773  elcncf  18790  icccvx  18846  iscmet3  19117  causs  19122  metcld2  19130  cmetss  19138  cncmet  19144  bcth3  19153  ovolgelb  19243  ovolfi  19257  shft2rab  19271  uniioombllem3  19344  dyadmax  19357  dyadmbl  19359  subopnmbl  19363  volcn  19365  mbfid  19395  mbfeqalem  19401  mbfres  19403  cnmbf  19418  i1fmulc  19462  mbfi1fseqlem3  19476  mbfi1fseqlem4  19477  itg2seq  19501  itg2gt0  19519  itgss3  19573  dvexp  19706  plypow  19991  plyeq0lem  19996  coeidlem  20023  dgrlt  20051  dgrcolem2  20059  elqaalem2  20104  aacjcl  20111  aaliou3lem1  20126  aaliou3lem2  20127  pserdvlem2  20211  abelthlem8  20222  cosord  20301  sinord  20303  resinf1o  20305  relogexp  20357  logdivlt  20383  advlogexp  20413  logcxp  20427  cxpcl  20432  rpcxpcl  20434  cxpne0  20435  birthdaylem2  20658  cxplim  20677  divsqrsumo1  20689  wilthlem1  20718  ftalem7  20728  basellem1  20730  sgmss  20756  issqf  20786  sqf11  20789  sgmf  20795  sgmnncl  20797  sqff1o  20832  dvdsflsumcom  20840  dvdsmulf1o  20846  sgmppw  20848  chtublem  20862  chtub  20863  logexprlim  20876  bposlem3  20937  bposlem5  20939  bposlem6  20940  lgsdirnn0  20990  lgsquad2  21011  lgsquad3  21012  dchrisumlem1  21050  dchrisumlem2  21051  dchrisumlem3  21052  mulogsumlem  21092  usgrafilem2  21292  cusgraexi  21343  cusgrafilem2  21355  hashnbgravdg  21530  nvo00  22110  nmorepnf  22117  ubthlem1  22220  normpyc  22496  occon3  22647  pjpreeq  22748  idcnop  23332  riesz3i  23413  cnlnssadj  23431  rnbra  23458  strlem3a  23603  cvcon3  23635  ssdmd1  23664  ssdmd2  23665  fzsplit3  23986  ishashinf  23997  esumcst  24251  dmvlsiga  24308  ballotlemimin  24542  zetacvg  24578  derangsn  24635  iscvm  24725  cvmsval  24732  cvmliftlem7  24757  cvmlift2lem12  24780  supfz  24978  zprod  25042  faclimlem3  25122  preduz  25224  predfz  25227  wfrlem10  25289  nobndlem2  25371  brbtwn  25552  bpolylem  25808  bpolysum  25813  bpolydiflem  25814  fsumkthpow  25816  nndivlub  25922  ltflcei  25950  lxflflp1  25952  opnrebl2  26015  nn0prpwlem  26016  tailval  26093  fzadd2  26136  caushft  26158  ismtyval  26200  heiborlem7  26217  heiborlem10  26220  heibor  26221  elrfirn  26440  ismrc  26446  nacsfix  26457  mzpcompact2lem  26499  eldiophb  26506  ellz1  26516  rexrabdioph  26545  rpexpmord  26702  congrep  26729  jm2.26a  26762  lindfmm  26966  rngunsnply  27047  mendrng  27169  expgrowthi  27219  cnfex  27367  itgsinexp  27417  4cycl2v2nb  27769  bnj545  28604  bnj929  28645  bnj953  28648
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