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  4119  unipw  4247  opeluu  4482  uniexb  4505  unon  4544  onintrab2im  4551  xpexg  4774  resiexg  4988  imaexg  5020  exse2  5040  soirri  5061  djudisj  5094  elxp5  5155  cnvexg  5204  cnviinm  5208  coexg  5211  funssres  5297  f1oabexg  5513  sefvex  5576  ssimaex  5619  mptfvex  5644  f1ompt  5710  fmptcof  5726  resfunexg  5780  mptexg  5784  funfvima3  5793  ovid  6036  ov  6039  ofres  6147  cofunexg  6163  opabex3d  6175  opabex3  6176  oprabexd  6181  1stcof  6218  2ndcof  6219  mpoexxg  6265  cnvf1o  6280  f2ndf  6281  algrflemg  6285  tposexg  6313  tfrlemisucaccv  6380  tfrlemibxssdm  6382  tfrlemibfn  6383  tfrlemi14d  6388  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemres  6404  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemres  6417  rdgtfr  6429  rdgruledefgg  6430  rdgon  6441  frecabex  6453  freccllem  6457  frecfcllem  6459  omcl  6516  oeicl  6517  erth  6635  th3qlem1  6693  mapex  6710  pmvalg  6715  mapsnconst  6750  ixpexgg  6778  fundmen  6862  cnvct  6865  snfig  6870  unen  6872  xpdom2  6887  mapxpen  6906  phplem2  6911  findcard2  6947  findcard2s  6948  infnfi  6953  relcnvfi  7002  sbthlemi8  7025  sbthlemi10  7027  fival  7031  fiss  7038  inl11  7126  casef  7149  caseinj  7150  caseinl  7152  caseinr  7153  djudom  7154  difinfsn  7161  djuinj  7167  0ct  7168  ctmlemr  7169  ctssdccl  7172  enomnilem  7199  enmkvlem  7222  enwomnilem  7230  djuassen  7279  xpdjuen  7280  djudoml  7281  djudomr  7282  cc2lem  7328  ltnnnq  7485  nnnq0lem1  7508  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemfl  7637  mulnqprlemfu  7638  suplocexprlem2b  7776  prsrlem1  7804  gt0srpr  7810  caucvgsrlemcl  7851  caucvgsrlemfv  7853  caucvgsrlembound  7856  mulcnsr  7897  mulcnsrec  7905  addvalex  7906  pitoregt0  7911  axmulass  7935  axdistr  7936  recriota  7952  mulrid  8018  axmulgt0  8093  cnegexlem2  8197  cnegex  8199  gt0ne0d  8533  recexre  8599  msqge0  8637  mulge0  8640  aptap  8671  recgt0  8871  recreclt  8921  cju  8982  nnge1  9007  nnnlt1  9010  nn0nlt0  9269  elz2  9391  nnm1ge0  9406  recnz  9413  zneo  9421  uz3m2nn  9641  eluz2b2  9671  nn01to3  9685  mnflt  9852  xnn0dcle  9871  xltadd1  9945  lincmb01cmp  10072  iccf1o  10073  fz1n  10113  fseq1p1m1  10163  fznn0  10182  fzctr  10202  4fvwrd4  10209  elfzonlteqm1  10280  divfl0  10368  modqelico  10408  zmodfz  10420  modqid  10423  modqmuladdim  10441  m1modge3gt1  10445  addmodid  10446  frec2uzf1od  10480  frecfzennn  10500  frecfzen2  10501  fzfig  10504  ser0  10607  ser3le  10611  expgt1  10651  expubnd  10670  iexpcyc  10718  binom2sub  10727  binom3  10731  zesq  10732  bernneq  10734  bernneq2  10735  expnbnd  10737  expnlbnd2  10739  facdiv  10812  faclbnd2  10816  faclbnd3  10817  bcval4  10826  hashinfom  10852  hashennn  10854  fihashf1rn  10862  isfinite4im  10866  hashfz  10895  iswrd  10919  iswrdiz  10924  wrdexg  10928  wrdexb  10929  wrdfin  10936  wrdnval  10947  wrdred1hash  10960  crre  11004  crim  11005  remim  11007  mulreap  11011  cjreb  11013  recj  11014  reneg  11015  readd  11016  remullem  11018  imcj  11022  imneg  11023  imadd  11024  cjadd  11031  cjneg  11037  imval2  11041  cjreim  11050  cnrecnv  11057  uzin2  11134  absval  11148  rennim  11149  resqrexlemcalc3  11163  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemgt0  11167  resqrexlemga  11170  absreimsq  11214  absreim  11215  amgm2  11265  climconst2  11437  climshft  11450  climshft2  11452  reccn2ap  11459  climge0  11471  sumsnf  11555  sumnul  11570  isumcl  11571  fsum2dlemstep  11580  fisumcom2  11584  fsumabs  11611  fsumiun  11623  binom  11630  bcxmas  11635  arisum  11644  expcnvap0  11648  explecnv  11651  geosergap  11652  geolim  11657  geolim2  11658  geo2sum  11660  geo2lim  11662  cvgratnnlemrate  11676  cvgratz  11678  mertenslemi1  11681  prodf1  11688  prodeq2w  11702  fprodntrivap  11730  prodsnf  11738  fprod2dlemstep  11768  fprodcom2fi  11772  efcllemp  11804  ege2le3  11817  eftlub  11836  efgt1  11843  tanval2ap  11859  tanval3ap  11860  resinval  11861  recosval  11862  efi4p  11863  resin4p  11864  recos4p  11865  resincl  11866  recoscl  11867  efmival  11879  efeul  11880  sinadd  11882  cosadd  11883  tanaddap  11885  sinmul  11890  cos2tsin  11897  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  sin01gt0  11908  cos01gt0  11909  absef  11916  absefib  11917  efieq1re  11918  demoivreALT  11920  eirraplem  11923  odd2np1  12017  oddm1even  12019  oddp1even  12020  oexpneg  12021  opoe  12039  omoe  12040  nn0o1gt2  12049  nn0o  12051  nninfctlemfo  12180  algcvg  12189  algcvgblem  12190  1nprm  12255  1idssfct  12256  oddprmge3  12276  divgcdodd  12284  pw2dvdslemn  12306  pw2dvds  12307  oddpwdclemodd  12313  oddpwdc  12315  phicl2  12355  phibndlem  12357  phibnd  12358  hashdvds  12362  crth  12365  phimullem  12366  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlema  12371  hashgcdeq  12380  phisum  12381  oddprm  12400  prm23ge5  12405  pythagtriplem1  12406  pythagtriplem4  12409  pythagtriplem12  12416  pythagtriplem14  12418  pczpre  12438  pcadd  12481  pcmpt  12484  pockthlem  12497  pockthi  12499  infpnlem2  12501  gzreim  12520  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem17  12548  evenennn  12553  ennnfonelemjn  12562  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemnn0  12582  exmidunben  12586  ctinfomlemom  12587  ssnnctlemct  12606  nninfdc  12613  slotex  12648  setscom  12661  setsslid  12672  basmex  12680  basmexd  12681  relelbasov  12683  ressbas2d  12689  ressbasid  12691  strressid  12692  ressval3d  12693  2strbas1g  12743  2strop1g  12744  rngbaseg  12756  rngplusgg  12757  rngmulrg  12758  srngbased  12767  srngplusgd  12768  srngmulrd  12769  srnginvld  12770  lmodbased  12785  lmodplusgd  12786  lmodscad  12787  lmodvscad  12788  ipsbased  12797  ipsaddgd  12798  ipsmulrd  12799  ipsscad  12800  ipsvscad  12801  ipsipd  12802  topgrpbasd  12817  topgrpplusgd  12818  topgrptsetd  12819  tgvalex  12877  prdsex  12883  imasex  12891  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfn  12903  imasaddval  12904  imasaddf  12905  imasmulfn  12906  imasmulval  12907  imasmulf  12908  qusval  12909  qusex  12911  qusaddvallemg  12919  qusaddflemg  12920  qusaddval  12921  qusaddf  12922  qusmulval  12923  qusmulf  12924  xpsfval  12934  xpsval  12938  plusffvalg  12948  grpidvalg  12959  igsumvalx  12975  gsumfzval  12977  gsumress  12981  gsum0g  12982  gsumval2  12983  issubmnd  13026  ress0g  13027  ismhm  13036  mhmex  13037  issubm  13047  0mhm  13061  grppropstrg  13094  grpinvfvalg  13117  grpinvval  13118  grpinvfng  13119  grpsubfvalg  13120  grpsubval  13121  grpressid  13136  grplactfval  13176  qusgrp2  13186  mulgfvalg  13194  mulgex  13196  mulgnngsum  13200  issubg  13246  subgex  13249  subgmulg  13261  issubg2m  13262  releqgg  13293  eqgex  13294  eqgfval  13295  eqgen  13300  isghm  13316  ablressid  13408  mgptopng  13428  rngressid  13453  qusrng  13457  dfur2g  13461  ringidss  13528  ring1  13558  ringressid  13562  qusring2  13565  reldvdsrsrg  13591  dvdsrvald  13592  dvdsrex  13597  unitgrp  13615  unitabl  13616  invrfvald  13621  unitlinv  13625  unitrinv  13626  dvrfvald  13632  rdivmuldivd  13643  invrpropdg  13648  rhmunitinv  13677  isnzr2  13683  issubrng  13698  issubrg  13720  subrgugrp  13739  subrgpropd  13752  rrgmex  13760  aprval  13781  islmod  13790  scaffvalg  13805  lssex  13853  lssmex  13854  lsssetm  13855  islssmg  13857  islss3  13878  lspfval  13887  lspval  13889  lspcl  13890  lspex  13894  sralemg  13937  srascag  13941  sravscag  13942  sraipg  13943  sraex  13945  rlmsubg  13957  rlmvnegg  13964  ixpsnbasval  13965  lidlvalg  13970  rspvalg  13971  lidlex  13972  rspex  13973  lidlmex  13974  lidlss  13975  lidlrsppropdg  13994  2idlmex  14000  qusrhm  14027  znlidl  14133  zncrng2  14134  znval  14135  znle  14136  znbaslemnn  14138  znbas  14143  znzrh2  14145  znzrhval  14146  znzrhfo  14147  zndvds  14148  znfi  14154  znhash  14155  znidom  14156  znidomb  14157  psrval  14163  psrbasg  14170  psrelbas  14171  psrplusgg  14173  psraddcl  14175  toponsspwpwg  14201  topgele  14208  istps  14211  topontopn  14216  tgclb  14244  lmfval  14371  lmres  14427  ispsmet  14502  psmetge0  14510  ismet  14523  isxmet  14524  xmetge0  14544  isxms2  14631  comet  14678  bdxmet  14680  cnmetdval  14708  cnbl0  14713  cnblcld  14714  reopnap  14725  tgioo  14733  cncfcncntop  14772  cncfmpt2fcntop  14778  maxcncf  14794  mincncf  14795  hovergt0  14829  limcimolemlt  14843  cnplimcim  14846  cnplimclemr  14848  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  dvfvalap  14860  dvbss  14864  dvcnp2cntop  14878  dvcn  14879  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvrecap  14892  dvmptfsum  14904  dveflem  14905  plyval  14911  plycolemc  14936  reeff1olem  14947  pilem3  14959  ef2kpi  14982  efper  14983  sinperlem  14984  efimpi  14995  ptolemy  15000  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  cosq14gt0  15008  tangtx  15014  sinkpi  15023  coskpi  15024  cosordlem  15025  rplogcl  15055  logge0  15056  logdivlti  15057  logbleb  15134  logblt  15135  binom4  15152  wilthlem1  15153  lgsval2lem  15167  lgsval4a  15179  lgsneg  15181  lgsdilem  15184  lgsdirprm  15191  lgsdirnn0  15204  gausslemma2dlem0i  15214  gausslemma2dlem6  15224  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlemofi  15233  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem2  15239  lgsquad2  15240  m1lgs  15242  2lgs  15261  2lgsoddprmlem2  15263  2lgsoddprm  15270  2sqlem2  15272  pwf1oexmid  15560  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612