Theorem syl2anr 476

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

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 |- ( ph -> ps )
2		syl2an.2	. . 3 |- ( ta -> ch )
3		syl2an.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	1, 2, 3	syl2an 475	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 451	1 |- ( ( ta /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  swopo  4724  funco  5534  resdif  5744  fvcofneq  5941  fnprb  6032  fnsuppresOLD  6033  isotr  6133  weisoeq  6152  brrpssg  6481  findsg  6626  coexg  6650  xpexgALT  6692  fnsuppres  6845  oaass  7128  oeword  7157  oeworde  7160  ixpssmapg  7418  pw2f1olem  7540  domsdomtr  7571  xpen  7599  mapen  7600  mapdom1  7601  mapfienlem1  7779  elfir  7790  wdomen2  7918  carden2b  8261  harcard  8272  isinffi  8286  acnlem  8342  acndom  8345  alephdom  8375  fin23lem21  8632  fin23lem39  8643  isf32lem5  8650  fin1a2lem12  8704  ttukeylem1  8802  pwcfsdom  8871  canthp1  8943  nqereu  9218  addpqf  9233  axmulf  9434  axmulass  9445  axdistr  9446  negeu  9723  fimaxre3  10408  nnsub  10491  nn0sub  10763  elz2  10798  uzaddcl  11057  qaddcl  11117  xltneg  11337  xleneg  11338  supxrbnd1  11434  infmxrgelb  11447  iccneg  11562  uzsubsubfz  11628  fzsplit2  11631  fzss1  11644  uzsplit  11672  fz0fzdiffz0  11705  difelfzle  11710  difelfznle  11711  fzonlt0  11743  fzouzsplit  11755  fzo0addelr  11770  eluzgtdifelfzo  11777  elfzodifsumelfzo  11781  ssfzo12  11804  elfznelfzob  11815  fllt  11842  flflp1  11843  uzsup  11890  negmod  11938  modifeq2int  11952  om2uzlt2i  11965  nn0ennn  11992  suppssfz  12003  seqfveq2  12032  sermono  12042  seqf1o  12051  ser1const  12066  faclbnd  12270  bcval4  12287  bcpasc  12301  hashkf  12309  hashunx  12357  hashfacen  12407  fz1isolem  12414  seqcoll  12416  hash2prd  12422  swrd0  12570  swrdfv2  12582  swrdspsleq  12585  swrdswrd  12596  swrdccatin12lem2  12625  swrdccat3  12628  revccat  12651  repswswrd  12667  cshwmodn  12677  cshwidxmod  12685  repswcshw  12691  2cshwid  12693  2cshwcom  12695  2cshwcshw  12704  cshwcshid  12706  cshwcsh2id  12707  s1co  12710  cshco  12713  trclub  12836  shftfval  12905  seqshft  12920  crim  12950  caubnd  13193  isercolllem2  13490  fsumcvg  13536  fsumcvg2  13551  fsumshftm  13598  fsumo1  13628  isumshft  13653  harmonic  13672  cvgrat  13694  mertenslem1  13695  zprod  13746  rpnnen2  13961  dvdsval3  13992  negdvdsb  14002  dvdsnegb  14003  dvdsmul1  14007  odd2np1  14048  divalglem8  14060  ndvdsadd  14068  dvdssqim  14193  nn0seqcvgd  14201  seq1st  14202  algcvgblem  14208  powm2modprm  14330  modprm0  14332  modprmn0modprm0  14334  pythagtriplem1  14342  pythagtriplem4  14345  pythagtriplem8  14349  pythagtriplem9  14350  pythagtriplem12  14352  pythagtriplem14  14354  pythagtriplem16  14356  pcexp  14385  pc2dvds  14404  pcz  14406  fldivp1  14418  pcfac  14420  pockthg  14426  infpnlem1  14430  prmreclem1  14436  prmreclem2  14437  1arith  14447  4sqlem11  14475  vdwlem2  14502  vdwlem8  14508  vdwnnlem2  14516  cshwshashlem2  14583  cshwshashlem3  14584  pwsval  14893  isacs1i  15064  funcsetcestrclem9  15549  ismgmid  16008  mhmpropd  16089  grpsubid1  16240  mulgnnp1  16267  mulgsubcl  16273  mulgnn0z  16279  mulgnndir  16281  mulgneg2  16286  lagsubg  16380  ghmco  16403  symg2bas  16540  symgextfv  16560  pgpfi2  16743  efgsfo  16874  frgpupf  16908  frgpup1  16910  gsummptshft  17072  telgsumfzslem  17130  telgsums  17135  ablfac1eu  17237  pgpfac1lem2  17239  ablfaclem3  17251  dvdsrid  17413  dvdsrneg  17416  dvr1  17451  abv1  17595  lbsexg  17923  gsummoncoe1  18459  xrsds  18574  znf1o  18681  lindfmm  18947  matecl  19012  mavmul0g  19140  gsummatr01  19246  mp2pm2mplem4  19395  chfacfisf  19440  chfacfisfcpmat  19441  chfacfpmmulgsum2  19451  cpmadugsumlemF  19462  isclo  19674  resttopon  19748  restcld  19759  restcls  19768  iscn  19822  iscnp  19824  cnco  19853  cndis  19878  cnindis  19879  cmpsub  19986  hauscmplem  19992  cmpfii  19995  ptcnplem  20207  txtube  20226  txcmplem1  20227  xkoptsub  20240  qtoptop  20286  kqfval  20309  hmeoco  20358  fileln0  20436  trfil1  20472  trfil2  20473  trufil  20496  elfm3  20536  hausflf2  20584  isucn  20866  bl2in  20988  metss2lem  21099  metss2  21100  stdbdxmet  21103  metrest  21112  nmfval2  21196  nmval2  21197  nmoix  21321  ioo2bl  21383  xrsxmet  21399  expcn  21461  elcncf  21478  icccvx  21535  iscmet3  21817  causs  21822  metcld2  21830  cmetss  21838  cncmet  21846  bcth3  21855  ovolgelb  21976  ovolfi  21990  shft2rab  22004  uniioombllem3  22079  dyadmax  22092  dyadmbl  22094  subopnmbl  22098  volcn  22100  mbfid  22128  mbfeqalem  22134  mbfres  22136  cnmbf  22151  i1fmulc  22195  mbfi1fseqlem3  22209  mbfi1fseqlem4  22210  itg2seq  22234  itg2gt0  22252  itgss3  22306  dvexp  22441  plypow  22687  plyeq0lem  22692  coeidlem  22719  dgrlt  22748  dgrcolem2  22756  elqaalem2  22801  aacjcl  22808  aaliou3lem1  22823  aaliou3lem2  22824  pserdvlem2  22908  abelthlem8  22919  cosord  23004  sinord  23006  resinf1o  23008  relogexp  23068  logdivlt  23093  advlogexp  23123  logcxp  23137  cxpcl  23142  rpcxpcl  23144  cxpne0  23145  logbchbase  23229  birthdaylem2  23399  cxplim  23418  divsqrtsumo1  23430  wilthlem1  23459  ftalem7  23469  basellem1  23471  sgmss  23497  issqf  23527  sqf11  23530  sgmf  23536  sgmnncl  23538  sqff1o  23573  dvdsflsumcom  23581  dvdsmulf1o  23587  sgmppw  23589  chtublem  23603  chtub  23604  logexprlim  23617  bposlem3  23678  bposlem5  23680  bposlem6  23681  lgsdirnn0  23731  lgsquad2  23752  lgsquad3  23753  dchrisumlem1  23791  dchrisumlem2  23792  dchrisumlem3  23793  mulogsumlem  23833  brbtwn  24323  usgrafilem2  24533  cusgraexi  24589  cusgrafilem2  24601  usgra2wlkspthlem2  24741  vfwlkniswwlkn  24827  clwlkisclwwlklem2fv2  24904  hashnbgravdg  25034  nbhashuvtx1  25036  rusgranumwlk  25078  4cycl2v2nb  25137  frg2woteqm  25180  2spotmdisj  25189  extwwlkfablem1  25195  numclwwlk8  25236  nvo00  25793  nmorepnf  25800  ubthlem1  25903  normpyc  26180  occon3  26332  pjpreeq  26433  idcnop  27016  riesz3i  27097  cnlnssadj  27115  rnbra  27142  strlem3a  27287  cvcon3  27319  ssdmd1  27348  ssdmd2  27349  relfi  27592  fzsplit3  27752  ishashinf  27759  esumcst  28211  dmvlsiga  28278  ballotlemimin  28627  zetacvg  28746  derangsn  28803  iscvm  28893  cvmsval  28900  cvmliftlem7  28925  cvmlift2lem12  28948  mclsssvlem  29111  supfz  29273  faclimlem3  29336  preduz  29445  predfz  29448  wfrlem10  29517  nobndlem2  29618  bpolylem  29963  bpolysum  29968  bpolydiflem  29969  fsumkthpow  29971  nndivlub  30076  finixpnum  30203  ltflcei  30208  mblfinlem2  30217  mblfinlem3  30218  mblfinlem4  30219  ftc1anclem1  30256  ftc1anclem4  30259  ftc1anclem5  30260  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  opnrebl2  30305  nn0prpwlem  30306  tailval  30357  fzadd2  30400  caushft  30420  ismtyval  30462  heiborlem7  30479  heiborlem10  30482  heibor  30483  impel  30669  elrfirn  30793  ismrc  30799  nacsfix  30810  mzpcompact2lem  30849  eldiophb  30855  ellz1  30865  rexrabdioph  30893  rpexpmord  31049  congrep  31076  jm2.26a  31108  rngunsnply  31290  mendring  31309  iocmbl  31348  isprm7  31360  expgrowthi  31406  cnfex  31570  icccncfext  31856  itgsinexp  31919  iblspltprt  31938  itgspltprt  31944  fourierdlem50  32105  fourierswlem  32179  etransclem35  32218  addlenpfx  32573  pfxccatin12lem2  32599  pfxccat3  32601  zm1nn  32646  ltsubnn0  32648  subsubelfzo0  32659  mgmhmpropd  32791  2zrngamgm  32945  lincresunit3  33282  lincreslvec3  33283  isldepslvec2  33286  m1modmmod  33334  blengt1fldiv2p1  33414  dignn0flhalf  33439  nn0sumshdiglemA  33440  aacllem  33550  bnj545  34300  bnj929  34341  bnj953  34344  rp-isfinite5  38172