Theorem sylancr 418

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancr.1	|- ps
sylancr.2	|- ( ph -> ch )
sylancr.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylancr	|- ( ph -> th )

Proof of Theorem sylancr

Step	Hyp	Ref	Expression
1		sylancr.1	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		sylancr.2	. 2 |- ( ph -> ch )
4		sylancr.3	. 2 |- ( ( ps /\ ch ) -> th )
5	2, 3, 4	syl2anc 415	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpteq2da  4215  unipw  4352  opeluu  4591  uniexb  4614  unon  4653  onintrab2im  4660  xpexg  4884  resiexg  5103  imaexg  5135  exse2  5156  soirri  5177  djudisj  5210  elxp5  5271  cnvexg  5320  cnviinm  5324  coexg  5327  funssres  5415  f1oabexg  5646  sefvex  5711  ssimaex  5758  mptfvex  5785  f1ompt  5850  fmptcof  5866  resfunexg  5927  mptexg  5933  funfvima3  5942  ovid  6195  ov  6198  ofres  6307  cofunexg  6328  opabex3d  6340  opabex3  6341  oprabexd  6350  1stcof  6387  2ndcof  6388  mpoexxg  6436  cnvf1o  6451  f2ndf  6452  algrflemg  6456  tposexg  6519  tfrlemisucaccv  6586  tfrlemibxssdm  6588  tfrlemibfn  6589  tfrlemi14d  6594  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemres  6610  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemres  6623  rdgtfr  6635  rdgruledefgg  6636  rdgon  6647  frecabex  6659  freccllem  6663  frecfcllem  6665  omcl  6724  oeicl  6725  erth  6843  th3qlem1  6901  mapex  6918  pmvalg  6923  mapfoss  6937  mapsnconst  6966  ixpexgg  6994  fundmen  7084  cnvct  7087  mapsnend  7089  snfig  7093  unen  7095  xpdom2  7119  mapxpen  7138  phplem2  7144  findcard2  7183  findcard2s  7184  infnfi  7189  relcnvfi  7245  sbthlemi8  7271  sbthlemi10  7273  fival  7294  fiss  7301  inl11  7395  casef  7418  caseinj  7419  caseinl  7421  caseinr  7422  djudom  7423  difinfsn  7430  djuinj  7436  0ct  7437  ctmlemr  7438  ctssdccl  7441  enomnilem  7468  enmkvlem  7491  enwomnilem  7499  djuassen  7563  xpdjuen  7564  djudoml  7565  djudomr  7566  cc2lem  7622  ltnnnq  7780  nnnq0lem1  7803  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemfl  7932  mulnqprlemfu  7933  suplocexprlem2b  8071  prsrlem1  8099  gt0srpr  8105  caucvgsrlemcl  8146  caucvgsrlemfv  8148  caucvgsrlembound  8151  mulcnsr  8192  mulcnsrec  8200  addvalex  8201  pitoregt0  8206  axmulass  8230  axdistr  8231  recriota  8247  mulrid  8313  axmulgt0  8387  cnegexlem2  8492  cnegex  8494  gt0ne0d  8830  recexre  8896  msqge0  8934  mulge0  8937  aptap  8968  recgt0  9170  recreclt  9220  cju  9281  nnge1  9306  nnnlt1  9309  nn0nlt0  9568  nnnle0  9672  elz2  9695  nnm1ge0  9711  recnz  9718  zneo  9726  uz3m2nn  9952  eluz2b2  9982  nn01to3  9996  mnflt  10164  xnn0dcle  10183  xltadd1  10257  lincmb01cmp  10384  iccf1o  10386  fz1n  10427  fseq1p1m1  10479  fznn0  10498  fzctr  10518  4fvwrd4  10525  fzo0n  10553  elfzonlteqm1  10606  divfl0  10709  modqelico  10749  zmodfz  10761  modqid  10764  modqmuladdim  10782  m1modge3gt1  10786  addmodid  10787  frec2uzf1od  10821  frecfzennn  10841  frecfzen2  10842  fzfig  10845  ser0  10948  ser3le  10952  expgt1  10992  expubnd  11011  iexpcyc  11059  binom2sub  11068  binom3  11072  zesq  11074  bernneq  11076  bernneq2  11077  expnbnd  11079  expnlbnd2  11081  facdiv  11154  faclbnd2  11158  faclbnd3  11159  bcval4  11168  hashinfom  11195  hashennn  11197  fihashf1rn  11205  isfinite4im  11209  hashfz  11240  ssenneg  11258  hashf1lem1  11263  hashf1lem2  11264  iswrd  11284  iswrdiz  11289  wrdexg  11293  wrdexb  11294  wrdfin  11301  wrdnval  11313  wrdred1hash  11326  ccatsymb  11348  ccatalpha  11359  s111  11377  fzowrddc  11397  swrdlen  11402  swrdwrdsymbg  11414  pfxval  11424  pfx0g  11426  fnpfx  11427  pfxlen  11435  cats1un  11471  swrdccat  11485  crre  11600  crim  11601  remim  11603  mulreap  11607  cjreb  11609  recj  11610  reneg  11611  readd  11612  remullem  11614  imcj  11618  imneg  11619  imadd  11620  cjadd  11627  cjneg  11633  imval2  11637  cjreim  11647  cnrecnv  11654  uzin2  11731  absval  11745  rennim  11746  resqrexlemcalc3  11760  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemgt0  11764  resqrexlemga  11767  absreimsq  11811  absreim  11812  amgm2  11862  climconst2  12035  climshft  12048  climshft2  12050  reccn2ap  12057  climge0  12069  sumsnf  12154  sumnul  12169  isumcl  12170  fsum2dlemstep  12179  fisumcom2  12183  fsumabs  12210  fsumiun  12222  binom  12229  bcxmas  12234  arisum  12243  expcnvap0  12247  explecnv  12250  geosergap  12251  geolim  12256  geolim2  12257  geo2sum  12259  geo2lim  12261  cvgratnnlemrate  12275  cvgratz  12277  mertenslemi1  12280  prodf1  12287  prodeq2w  12301  fprodntrivap  12329  prodsnf  12337  fprod2dlemstep  12367  fprodcom2fi  12371  efcllemp  12403  ege2le3  12416  eftlub  12435  efgt1  12442  tanval2ap  12458  tanval3ap  12459  resinval  12460  recosval  12461  efi4p  12462  resin4p  12463  recos4p  12464  resincl  12465  recoscl  12466  efmival  12478  efeul  12479  sinadd  12481  cosadd  12482  tanaddap  12484  sinmul  12489  cos2tsin  12496  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  cos01gt0  12508  absef  12515  absefib  12516  efieq1re  12517  demoivreALT  12519  eirraplem  12522  3dvds  12609  odd2np1  12618  oddm1even  12620  oddp1even  12621  oexpneg  12622  opoe  12640  omoe  12641  nn0o1gt2  12650  nn0o  12652  bitsdc  12692  bitsfzolem  12699  bitsfzo  12700  bitsinv1lem  12706  bitsinv1  12707  nninfctlemfo  12795  algcvg  12804  algcvgblem  12805  1nprm  12870  1idssfct  12871  oddprmge3  12891  divgcdodd  12899  pw2dvdslemn  12921  pw2dvds  12922  oddpwdclemodd  12928  oddpwdc  12930  phicl2  12970  phibndlem  12972  phibnd  12973  hashdvds  12977  crth  12980  phimullem  12981  eulerthlemfi  12984  eulerthlemrprm  12985  eulerthlema  12986  hashgcdeq  12996  phisum  12997  oddprm  13016  prm23ge5  13021  pythagtriplem1  13022  pythagtriplem4  13025  pythagtriplem12  13032  pythagtriplem14  13034  pczpre  13054  pcadd  13097  pcmpt  13100  pockthlem  13113  pockthi  13115  infpnlem2  13117  gzreim  13136  4sqlem11  13158  4sqlem12  13159  4sqlem13m  13160  4sqlem17  13164  2expltfac  13196  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemefi  13215  ballotfilemodife  13218  ballotfilem4  13219  evenennn  13262  ennnfonelemjn  13271  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemnn0  13291  exmidunben  13295  ctinfomlemom  13296  ssnnctlemct  13315  nninfdc  13322  slotex  13357  setscom  13370  strslfv3  13376  setsslid  13381  bassetsnn  13387  basmex  13390  basmexd  13391  relelbasov  13393  ressbas2d  13399  ressbasid  13401  strressid  13402  ressval3d  13403  2strbas1g  13454  2strop1g  13455  rngbaseg  13467  rngplusgg  13468  rngmulrg  13469  srngbased  13478  srngplusgd  13479  srngmulrd  13480  srnginvld  13481  lmodbased  13496  lmodplusgd  13497  lmodscad  13498  lmodvscad  13499  ipsbased  13508  ipsaddgd  13509  ipsmulrd  13510  ipsscad  13511  ipsvscad  13512  ipsipd  13513  topgrpbasd  13528  topgrpplusgd  13529  topgrptsetd  13530  tgvalex  13594  imasex  13603  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfn  13615  imasaddval  13616  imasaddf  13617  imasmulfn  13618  imasmulval  13619  imasmulf  13620  qusval  13621  qusex  13623  qusaddvallemg  13631  qusaddflemg  13632  qusaddval  13633  qusaddf  13634  qusmulval  13635  qusmulf  13636  xpsfval  13646  plusffvalg  13659  grpidvalg  13670  gzsumvalx  13686  gzsumfzval  13688  gzsumress  13689  gzsum0  13690  gzsumval2  13691  issubmnd  13732  ress0g  13733  ismhm  13745  mhmex  13746  issubm  13756  0mhm  13770  grppropstrg  13801  grpinvfvalg  13824  grpinvval  13825  grpinvfng  13826  grpsubfvalg  13827  grpsubval  13828  grpressid  13843  grplactfval  13883  qusgrp2  13893  mulgfvalg  13901  mulgex  13903  mulgnngzsum  13907  issubg  13953  subgex  13956  subgmulg  13968  issubg2m  13969  releqgg  14000  eqgex  14001  eqgfval  14002  eqgen  14007  isghm  14023  ablressid  14116  gsumsncmn  14133  gsump1  14134  gsummptfidmadd  14138  prdsex  14149  prdsval  14150  prdsbaslemss  14151  prdsbas  14153  prdsplusg  14154  prdsmulr  14155  xpsval  14178  pwsbas  14182  pwselbasb  14183  pwssnf1o  14188  mgptopng  14203  rngressid  14228  qusrng  14232  dfur2g  14240  ringidss  14307  ring1  14337  ringressid  14341  qusring2  14344  opprringb  14359  dvdsrvald  14373  dvdsrex  14378  unitgrp  14396  unitabl  14397  invrfvald  14402  unitlinv  14406  unitrinv  14407  dvrfvald  14413  rdivmuldivd  14424  invrpropdg  14429  rhmunitinv  14458  isnzr2  14464  issubrng  14480  issubrg  14502  subrgugrp  14521  subrgpropd  14534  rrgmex  14542  aprval  14564  aprprop  14574  islmod  14600  scaffvalg  14615  lssex  14663  lssmex  14664  lsssetm  14665  islssmg  14667  islss3  14688  lspfval  14697  lspval  14699  lspcl  14700  lspex  14704  sralemg  14747  srascag  14751  sravscag  14752  sraipg  14753  sraex  14755  rlmsubg  14767  rlmvnegg  14774  ixpsnbasval  14775  lidlvalg  14780  rspvalg  14781  lidlex  14782  rspex  14783  lidlmex  14784  lidlss  14785  lidlrsppropdg  14804  2idlmex  14810  qusrhm  14837  gsumfsum  14895  znlidl  14941  zncrng2  14942  znval  14943  znle  14944  znbaslemnn  14946  znbas  14951  znzrh2  14953  znzrhval  14954  znzrhfo  14955  zndvds  14956  znfi  14962  znhash  14963  znidom  14964  znidomb  14965  psrval  14973  psrbasg  14988  psrelbas  14989  psrplusgg  14992  psraddcl  14994  psr0cl  14995  psrnegcl  14997  psr1clfi  15002  mplvalcoe  15004  mplplusgg  15017  toponsspwpwg  15046  topgele  15053  istps  15056  topontopn  15061  tgclb  15089  lmfval  15217  lmres  15272  ispsmet  15347  psmetge0  15355  ismet  15368  isxmet  15369  xmetge0  15389  isxms2  15476  comet  15523  bdxmet  15525  cnmetdval  15553  cnbl0  15558  cnblcld  15559  reopnap  15570  tgioo  15578  cncfcncntop  15617  cncfmpt2fcntop  15623  maxcncf  15639  mincncf  15640  hovergt0  15674  limcimolemlt  15688  cnplimcim  15691  cnplimclemr  15693  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  dvfvalap  15705  dvbss  15709  dvcnp2cntop  15723  dvcn  15724  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvrecap  15737  dvmptfsum  15749  dveflem  15750  plyval  15756  plycolemc  15782  dvply2  15791  reeff1olem  15795  pilem3  15807  ef2kpi  15830  efper  15831  sinperlem  15832  efimpi  15843  ptolemy  15848  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  cosq14gt0  15856  tangtx  15862  sinkpi  15871  coskpi  15872  cosordlem  15873  rplogcl  15903  logge0  15904  logdivlti  15905  logbleb  15986  logblt  15987  binom4  16004  wilthlem1  16008  1sgmprm  16022  1sgm2ppw  16023  mersenne  16025  perfect1  16026  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgsval2lem  16043  lgsval4a  16055  lgsneg  16057  lgsdilem  16060  lgsdirprm  16067  lgsdirnn0  16080  gausslemma2dlem0i  16090  gausslemma2dlem6  16100  gausslemma2dlem7  16101  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlemofi  16109  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem2  16115  lgsquad2  16116  m1lgs  16118  2lgs  16137  2lgsoddprmlem2  16139  2lgsoddprm  16146  2sqlem2  16148  vtxvalg  16171  vtxex  16173  struct2slots2dom  16193  structvtxval  16194  structiedg0val  16195  structgrssvtx  16197  structgrssiedg  16198  edgstruct  16219  vdegp1bid  16470  wlkv0  16524  upgr2wlkdc  16532  clwwlkex  16553  clwwlkccatlem  16555  eupthfi  16606  trlsegvdeglem6  16620  konigsberglem1  16643  konigsberglem5  16647  depindlem1  16661  pwf1oexmid  16943  nnnninfex  16970  repiecege0  16981  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007