Theorem sylancr 414

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 411	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  4123  unipw  4251  opeluu  4486  uniexb  4509  unon  4548  onintrab2im  4555  xpexg  4778  resiexg  4992  imaexg  5024  exse2  5044  soirri  5065  djudisj  5098  elxp5  5159  cnvexg  5208  cnviinm  5212  coexg  5215  funssres  5301  f1oabexg  5519  sefvex  5582  ssimaex  5625  mptfvex  5650  f1ompt  5716  fmptcof  5732  resfunexg  5786  mptexg  5790  funfvima3  5799  ovid  6043  ov  6046  ofres  6154  cofunexg  6175  opabex3d  6187  opabex3  6188  oprabexd  6193  1stcof  6230  2ndcof  6231  mpoexxg  6277  cnvf1o  6292  f2ndf  6293  algrflemg  6297  tposexg  6325  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemi14d  6400  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemres  6429  rdgtfr  6441  rdgruledefgg  6442  rdgon  6453  frecabex  6465  freccllem  6469  frecfcllem  6471  omcl  6528  oeicl  6529  erth  6647  th3qlem1  6705  mapex  6722  pmvalg  6727  mapsnconst  6762  ixpexgg  6790  fundmen  6874  cnvct  6877  snfig  6882  unen  6884  xpdom2  6899  mapxpen  6918  phplem2  6923  findcard2  6959  findcard2s  6960  infnfi  6965  relcnvfi  7016  sbthlemi8  7039  sbthlemi10  7041  fival  7045  fiss  7052  inl11  7140  casef  7163  caseinj  7164  caseinl  7166  caseinr  7167  djudom  7168  difinfsn  7175  djuinj  7181  0ct  7182  ctmlemr  7183  ctssdccl  7186  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  djuassen  7300  xpdjuen  7301  djudoml  7302  djudomr  7303  cc2lem  7349  ltnnnq  7507  nnnq0lem1  7530  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemfl  7659  mulnqprlemfu  7660  suplocexprlem2b  7798  prsrlem1  7826  gt0srpr  7832  caucvgsrlemcl  7873  caucvgsrlemfv  7875  caucvgsrlembound  7878  mulcnsr  7919  mulcnsrec  7927  addvalex  7928  pitoregt0  7933  axmulass  7957  axdistr  7958  recriota  7974  mulrid  8040  axmulgt0  8115  cnegexlem2  8219  cnegex  8221  gt0ne0d  8556  recexre  8622  msqge0  8660  mulge0  8663  aptap  8694  recgt0  8894  recreclt  8944  cju  9005  nnge1  9030  nnnlt1  9033  nn0nlt0  9292  elz2  9414  nnm1ge0  9429  recnz  9436  zneo  9444  uz3m2nn  9664  eluz2b2  9694  nn01to3  9708  mnflt  9875  xnn0dcle  9894  xltadd1  9968  lincmb01cmp  10095  iccf1o  10096  fz1n  10136  fseq1p1m1  10186  fznn0  10205  fzctr  10225  4fvwrd4  10232  elfzonlteqm1  10303  divfl0  10403  modqelico  10443  zmodfz  10455  modqid  10458  modqmuladdim  10476  m1modge3gt1  10480  addmodid  10481  frec2uzf1od  10515  frecfzennn  10535  frecfzen2  10536  fzfig  10539  ser0  10642  ser3le  10646  expgt1  10686  expubnd  10705  iexpcyc  10753  binom2sub  10762  binom3  10766  zesq  10767  bernneq  10769  bernneq2  10770  expnbnd  10772  expnlbnd2  10774  facdiv  10847  faclbnd2  10851  faclbnd3  10852  bcval4  10861  hashinfom  10887  hashennn  10889  fihashf1rn  10897  isfinite4im  10901  hashfz  10930  iswrd  10954  iswrdiz  10959  wrdexg  10963  wrdexb  10964  wrdfin  10971  wrdnval  10982  wrdred1hash  10995  crre  11039  crim  11040  remim  11042  mulreap  11046  cjreb  11048  recj  11049  reneg  11050  readd  11051  remullem  11053  imcj  11057  imneg  11058  imadd  11059  cjadd  11066  cjneg  11072  imval2  11076  cjreim  11085  cnrecnv  11092  uzin2  11169  absval  11183  rennim  11184  resqrexlemcalc3  11198  resqrexlemnm  11200  resqrexlemcvg  11201  resqrexlemgt0  11202  resqrexlemga  11205  absreimsq  11249  absreim  11250  amgm2  11300  climconst2  11473  climshft  11486  climshft2  11488  reccn2ap  11495  climge0  11507  sumsnf  11591  sumnul  11606  isumcl  11607  fsum2dlemstep  11616  fisumcom2  11620  fsumabs  11647  fsumiun  11659  binom  11666  bcxmas  11671  arisum  11680  expcnvap0  11684  explecnv  11687  geosergap  11688  geolim  11693  geolim2  11694  geo2sum  11696  geo2lim  11698  cvgratnnlemrate  11712  cvgratz  11714  mertenslemi1  11717  prodf1  11724  prodeq2w  11738  fprodntrivap  11766  prodsnf  11774  fprod2dlemstep  11804  fprodcom2fi  11808  efcllemp  11840  ege2le3  11853  eftlub  11872  efgt1  11879  tanval2ap  11895  tanval3ap  11896  resinval  11897  recosval  11898  efi4p  11899  resin4p  11900  recos4p  11901  resincl  11902  recoscl  11903  efmival  11915  efeul  11916  sinadd  11918  cosadd  11919  tanaddap  11921  sinmul  11926  cos2tsin  11933  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  sin01gt0  11944  cos01gt0  11945  absef  11952  absefib  11953  efieq1re  11954  demoivreALT  11956  eirraplem  11959  3dvds  12046  odd2np1  12055  oddm1even  12057  oddp1even  12058  oexpneg  12059  opoe  12077  omoe  12078  nn0o1gt2  12087  nn0o  12089  bitsdc  12129  bitsfzolem  12136  bitsfzo  12137  bitsinv1lem  12143  bitsinv1  12144  nninfctlemfo  12232  algcvg  12241  algcvgblem  12242  1nprm  12307  1idssfct  12308  oddprmge3  12328  divgcdodd  12336  pw2dvdslemn  12358  pw2dvds  12359  oddpwdclemodd  12365  oddpwdc  12367  phicl2  12407  phibndlem  12409  phibnd  12410  hashdvds  12414  crth  12417  phimullem  12418  eulerthlemfi  12421  eulerthlemrprm  12422  eulerthlema  12423  hashgcdeq  12433  phisum  12434  oddprm  12453  prm23ge5  12458  pythagtriplem1  12459  pythagtriplem4  12462  pythagtriplem12  12469  pythagtriplem14  12471  pczpre  12491  pcadd  12534  pcmpt  12537  pockthlem  12550  pockthi  12552  infpnlem2  12554  gzreim  12573  4sqlem11  12595  4sqlem12  12596  4sqlem13m  12597  4sqlem17  12601  2expltfac  12633  evenennn  12635  ennnfonelemjn  12644  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemnn0  12664  exmidunben  12668  ctinfomlemom  12669  ssnnctlemct  12688  nninfdc  12695  slotex  12730  setscom  12743  strslfv3  12749  setsslid  12754  basmex  12762  basmexd  12763  relelbasov  12765  ressbas2d  12771  ressbasid  12773  strressid  12774  ressval3d  12775  2strbas1g  12825  2strop1g  12826  rngbaseg  12838  rngplusgg  12839  rngmulrg  12840  srngbased  12849  srngplusgd  12850  srngmulrd  12851  srnginvld  12852  lmodbased  12867  lmodplusgd  12868  lmodscad  12869  lmodvscad  12870  ipsbased  12879  ipsaddgd  12880  ipsmulrd  12881  ipsscad  12882  ipsvscad  12883  ipsipd  12884  topgrpbasd  12899  topgrpplusgd  12900  topgrptsetd  12901  tgvalex  12965  prdsex  12971  prdsval  12975  prdsbaslemss  12976  prdsbas  12978  prdsplusg  12979  prdsmulr  12980  pwsbas  12994  pwselbasb  12995  pwssnf1o  13000  imasex  13007  imasival  13008  imasbas  13009  imasplusg  13010  imasmulr  13011  imasaddfn  13019  imasaddval  13020  imasaddf  13021  imasmulfn  13022  imasmulval  13023  imasmulf  13024  qusval  13025  qusex  13027  qusaddvallemg  13035  qusaddflemg  13036  qusaddval  13037  qusaddf  13038  qusmulval  13039  qusmulf  13040  xpsfval  13050  xpsval  13054  plusffvalg  13064  grpidvalg  13075  igsumvalx  13091  gsumfzval  13093  gsumress  13097  gsum0g  13098  gsumval2  13099  issubmnd  13144  ress0g  13145  ismhm  13163  mhmex  13164  issubm  13174  0mhm  13188  grppropstrg  13221  grpinvfvalg  13244  grpinvval  13245  grpinvfng  13246  grpsubfvalg  13247  grpsubval  13248  grpressid  13263  grplactfval  13303  qusgrp2  13319  mulgfvalg  13327  mulgex  13329  mulgnngsum  13333  issubg  13379  subgex  13382  subgmulg  13394  issubg2m  13395  releqgg  13426  eqgex  13427  eqgfval  13428  eqgen  13433  isghm  13449  ablressid  13541  mgptopng  13561  rngressid  13586  qusrng  13590  dfur2g  13594  ringidss  13661  ring1  13691  ringressid  13695  qusring2  13698  reldvdsrsrg  13724  dvdsrvald  13725  dvdsrex  13730  unitgrp  13748  unitabl  13749  invrfvald  13754  unitlinv  13758  unitrinv  13759  dvrfvald  13765  rdivmuldivd  13776  invrpropdg  13781  rhmunitinv  13810  isnzr2  13816  issubrng  13831  issubrg  13853  subrgugrp  13872  subrgpropd  13885  rrgmex  13893  aprval  13914  islmod  13923  scaffvalg  13938  lssex  13986  lssmex  13987  lsssetm  13988  islssmg  13990  islss3  14011  lspfval  14020  lspval  14022  lspcl  14023  lspex  14027  sralemg  14070  srascag  14074  sravscag  14075  sraipg  14076  sraex  14078  rlmsubg  14090  rlmvnegg  14097  ixpsnbasval  14098  lidlvalg  14103  rspvalg  14104  lidlex  14105  rspex  14106  lidlmex  14107  lidlss  14108  lidlrsppropdg  14127  2idlmex  14133  qusrhm  14160  znlidl  14266  zncrng2  14267  znval  14268  znle  14269  znbaslemnn  14271  znbas  14276  znzrh2  14278  znzrhval  14279  znzrhfo  14280  zndvds  14281  znfi  14287  znhash  14288  znidom  14289  znidomb  14290  psrval  14296  psrbasg  14303  psrelbas  14304  psrplusgg  14306  psraddcl  14308  psr0cl  14309  psrnegcl  14311  psr1clfi  14316  toponsspwpwg  14342  topgele  14349  istps  14352  topontopn  14357  tgclb  14385  lmfval  14512  lmres  14568  ispsmet  14643  psmetge0  14651  ismet  14664  isxmet  14665  xmetge0  14685  isxms2  14772  comet  14819  bdxmet  14821  cnmetdval  14849  cnbl0  14854  cnblcld  14855  reopnap  14866  tgioo  14874  cncfcncntop  14913  cncfmpt2fcntop  14919  maxcncf  14935  mincncf  14936  hovergt0  14970  limcimolemlt  14984  cnplimcim  14987  cnplimclemr  14989  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  dvfvalap  15001  dvbss  15005  dvcnp2cntop  15019  dvcn  15020  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvrecap  15033  dvmptfsum  15045  dveflem  15046  plyval  15052  plycolemc  15078  dvply2  15087  reeff1olem  15091  pilem3  15103  ef2kpi  15126  efper  15127  sinperlem  15128  efimpi  15139  ptolemy  15144  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  cosq14gt0  15152  tangtx  15158  sinkpi  15167  coskpi  15168  cosordlem  15169  rplogcl  15199  logge0  15200  logdivlti  15201  logbleb  15281  logblt  15282  binom4  15299  wilthlem1  15300  1sgmprm  15314  1sgm2ppw  15315  mersenne  15317  perfect1  15318  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgsval2lem  15335  lgsval4a  15347  lgsneg  15349  lgsdilem  15352  lgsdirprm  15359  lgsdirnn0  15372  gausslemma2dlem0i  15382  gausslemma2dlem6  15392  gausslemma2dlem7  15393  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlemofi  15401  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem2  15407  lgsquad2  15408  m1lgs  15410  2lgs  15429  2lgsoddprmlem2  15431  2lgsoddprm  15438  2sqlem2  15440  pwf1oexmid  15730  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783