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  4176  unipw  4307  opeluu  4545  uniexb  4568  unon  4607  onintrab2im  4614  xpexg  4838  resiexg  5056  imaexg  5088  exse2  5108  soirri  5129  djudisj  5162  elxp5  5223  cnvexg  5272  cnviinm  5276  coexg  5279  funssres  5366  f1oabexg  5592  sefvex  5656  ssimaex  5703  mptfvex  5728  f1ompt  5794  fmptcof  5810  resfunexg  5870  mptexg  5874  funfvima3  5883  ovid  6133  ov  6136  ofres  6245  cofunexg  6266  opabex3d  6278  opabex3  6279  oprabexd  6284  1stcof  6321  2ndcof  6322  mpoexxg  6370  cnvf1o  6385  f2ndf  6386  algrflemg  6390  tposexg  6419  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemi14d  6494  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemres  6523  rdgtfr  6535  rdgruledefgg  6536  rdgon  6547  frecabex  6559  freccllem  6563  frecfcllem  6565  omcl  6624  oeicl  6625  erth  6743  th3qlem1  6801  mapex  6818  pmvalg  6823  mapsnconst  6858  ixpexgg  6886  fundmen  6976  cnvct  6979  snfig  6984  unen  6986  xpdom2  7010  mapxpen  7029  phplem2  7034  findcard2  7071  findcard2s  7072  infnfi  7077  relcnvfi  7131  sbthlemi8  7154  sbthlemi10  7156  fival  7160  fiss  7167  inl11  7255  casef  7278  caseinj  7279  caseinl  7281  caseinr  7282  djudom  7283  difinfsn  7290  djuinj  7296  0ct  7297  ctmlemr  7298  ctssdccl  7301  enomnilem  7328  enmkvlem  7351  enwomnilem  7359  djuassen  7422  xpdjuen  7423  djudoml  7424  djudomr  7425  cc2lem  7475  ltnnnq  7633  nnnq0lem1  7656  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemfl  7785  mulnqprlemfu  7786  suplocexprlem2b  7924  prsrlem1  7952  gt0srpr  7958  caucvgsrlemcl  7999  caucvgsrlemfv  8001  caucvgsrlembound  8004  mulcnsr  8045  mulcnsrec  8053  addvalex  8054  pitoregt0  8059  axmulass  8083  axdistr  8084  recriota  8100  mulrid  8166  axmulgt0  8241  cnegexlem2  8345  cnegex  8347  gt0ne0d  8682  recexre  8748  msqge0  8786  mulge0  8789  aptap  8820  recgt0  9020  recreclt  9070  cju  9131  nnge1  9156  nnnlt1  9159  nn0nlt0  9418  nnnle0  9518  elz2  9541  nnm1ge0  9556  recnz  9563  zneo  9571  uz3m2nn  9797  eluz2b2  9827  nn01to3  9841  mnflt  10008  xnn0dcle  10027  xltadd1  10101  lincmb01cmp  10228  iccf1o  10229  fz1n  10269  fseq1p1m1  10319  fznn0  10338  fzctr  10358  4fvwrd4  10365  fzo0n  10393  elfzonlteqm1  10445  divfl0  10546  modqelico  10586  zmodfz  10598  modqid  10601  modqmuladdim  10619  m1modge3gt1  10623  addmodid  10624  frec2uzf1od  10658  frecfzennn  10678  frecfzen2  10679  fzfig  10682  ser0  10785  ser3le  10789  expgt1  10829  expubnd  10848  iexpcyc  10896  binom2sub  10905  binom3  10909  zesq  10910  bernneq  10912  bernneq2  10913  expnbnd  10915  expnlbnd2  10917  facdiv  10990  faclbnd2  10994  faclbnd3  10995  bcval4  11004  hashinfom  11030  hashennn  11032  fihashf1rn  11040  isfinite4im  11044  hashfz  11075  iswrd  11105  iswrdiz  11110  wrdexg  11114  wrdexb  11115  wrdfin  11122  wrdnval  11134  wrdred1hash  11147  ccatsymb  11169  ccatalpha  11180  s111  11198  fzowrddc  11218  swrdlen  11223  swrdwrdsymbg  11235  pfxval  11245  pfx0g  11247  fnpfx  11248  pfxlen  11256  cats1un  11292  swrdccat  11306  crre  11408  crim  11409  remim  11411  mulreap  11415  cjreb  11417  recj  11418  reneg  11419  readd  11420  remullem  11422  imcj  11426  imneg  11427  imadd  11428  cjadd  11435  cjneg  11441  imval2  11445  cjreim  11454  cnrecnv  11461  uzin2  11538  absval  11552  rennim  11553  resqrexlemcalc3  11567  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemgt0  11571  resqrexlemga  11574  absreimsq  11618  absreim  11619  amgm2  11669  climconst2  11842  climshft  11855  climshft2  11857  reccn2ap  11864  climge0  11876  sumsnf  11960  sumnul  11975  isumcl  11976  fsum2dlemstep  11985  fisumcom2  11989  fsumabs  12016  fsumiun  12028  binom  12035  bcxmas  12040  arisum  12049  expcnvap0  12053  explecnv  12056  geosergap  12057  geolim  12062  geolim2  12063  geo2sum  12065  geo2lim  12067  cvgratnnlemrate  12081  cvgratz  12083  mertenslemi1  12086  prodf1  12093  prodeq2w  12107  fprodntrivap  12135  prodsnf  12143  fprod2dlemstep  12173  fprodcom2fi  12177  efcllemp  12209  ege2le3  12222  eftlub  12241  efgt1  12248  tanval2ap  12264  tanval3ap  12265  resinval  12266  recosval  12267  efi4p  12268  resin4p  12269  recos4p  12270  resincl  12271  recoscl  12272  efmival  12284  efeul  12285  sinadd  12287  cosadd  12288  tanaddap  12290  sinmul  12295  cos2tsin  12302  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  cos01gt0  12314  absef  12321  absefib  12322  efieq1re  12323  demoivreALT  12325  eirraplem  12328  3dvds  12415  odd2np1  12424  oddm1even  12426  oddp1even  12427  oexpneg  12428  opoe  12446  omoe  12447  nn0o1gt2  12456  nn0o  12458  bitsdc  12498  bitsfzolem  12505  bitsfzo  12506  bitsinv1lem  12512  bitsinv1  12513  nninfctlemfo  12601  algcvg  12610  algcvgblem  12611  1nprm  12676  1idssfct  12677  oddprmge3  12697  divgcdodd  12705  pw2dvdslemn  12727  pw2dvds  12728  oddpwdclemodd  12734  oddpwdc  12736  phicl2  12776  phibndlem  12778  phibnd  12779  hashdvds  12783  crth  12786  phimullem  12787  eulerthlemfi  12790  eulerthlemrprm  12791  eulerthlema  12792  hashgcdeq  12802  phisum  12803  oddprm  12822  prm23ge5  12827  pythagtriplem1  12828  pythagtriplem4  12831  pythagtriplem12  12838  pythagtriplem14  12840  pczpre  12860  pcadd  12903  pcmpt  12906  pockthlem  12919  pockthi  12921  infpnlem2  12923  gzreim  12942  4sqlem11  12964  4sqlem12  12965  4sqlem13m  12966  4sqlem17  12970  2expltfac  13002  evenennn  13004  ennnfonelemjn  13013  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemnn0  13033  exmidunben  13037  ctinfomlemom  13038  ssnnctlemct  13057  nninfdc  13064  slotex  13099  setscom  13112  strslfv3  13118  setsslid  13123  bassetsnn  13129  basmex  13132  basmexd  13133  relelbasov  13135  ressbas2d  13141  ressbasid  13143  strressid  13144  ressval3d  13145  2strbas1g  13196  2strop1g  13197  rngbaseg  13209  rngplusgg  13210  rngmulrg  13211  srngbased  13220  srngplusgd  13221  srngmulrd  13222  srnginvld  13223  lmodbased  13238  lmodplusgd  13239  lmodscad  13240  lmodvscad  13241  ipsbased  13250  ipsaddgd  13251  ipsmulrd  13252  ipsscad  13253  ipsvscad  13254  ipsipd  13255  topgrpbasd  13270  topgrpplusgd  13271  topgrptsetd  13272  tgvalex  13336  prdsex  13342  prdsval  13346  prdsbaslemss  13347  prdsbas  13349  prdsplusg  13350  prdsmulr  13351  pwsbas  13365  pwselbasb  13366  pwssnf1o  13371  imasex  13378  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfn  13390  imasaddval  13391  imasaddf  13392  imasmulfn  13393  imasmulval  13394  imasmulf  13395  qusval  13396  qusex  13398  qusaddvallemg  13406  qusaddflemg  13407  qusaddval  13408  qusaddf  13409  qusmulval  13410  qusmulf  13411  xpsfval  13421  xpsval  13425  plusffvalg  13435  grpidvalg  13446  igsumvalx  13462  gsumfzval  13464  gsumress  13468  gsum0g  13469  gsumval2  13470  issubmnd  13515  ress0g  13516  ismhm  13534  mhmex  13535  issubm  13545  0mhm  13559  grppropstrg  13592  grpinvfvalg  13615  grpinvval  13616  grpinvfng  13617  grpsubfvalg  13618  grpsubval  13619  grpressid  13634  grplactfval  13674  qusgrp2  13690  mulgfvalg  13698  mulgex  13700  mulgnngsum  13704  issubg  13750  subgex  13753  subgmulg  13765  issubg2m  13766  releqgg  13797  eqgex  13798  eqgfval  13799  eqgen  13804  isghm  13820  ablressid  13912  mgptopng  13932  rngressid  13957  qusrng  13961  dfur2g  13965  ringidss  14032  ring1  14062  ringressid  14066  qusring2  14069  dvdsrvald  14097  dvdsrex  14102  unitgrp  14120  unitabl  14121  invrfvald  14126  unitlinv  14130  unitrinv  14131  dvrfvald  14137  rdivmuldivd  14148  invrpropdg  14153  rhmunitinv  14182  isnzr2  14188  issubrng  14203  issubrg  14225  subrgugrp  14244  subrgpropd  14257  rrgmex  14265  aprval  14286  islmod  14295  scaffvalg  14310  lssex  14358  lssmex  14359  lsssetm  14360  islssmg  14362  islss3  14383  lspfval  14392  lspval  14394  lspcl  14395  lspex  14399  sralemg  14442  srascag  14446  sravscag  14447  sraipg  14448  sraex  14450  rlmsubg  14462  rlmvnegg  14469  ixpsnbasval  14470  lidlvalg  14475  rspvalg  14476  lidlex  14477  rspex  14478  lidlmex  14479  lidlss  14480  lidlrsppropdg  14499  2idlmex  14505  qusrhm  14532  znlidl  14638  zncrng2  14639  znval  14640  znle  14641  znbaslemnn  14643  znbas  14648  znzrh2  14650  znzrhval  14651  znzrhfo  14652  zndvds  14653  znfi  14659  znhash  14660  znidom  14661  znidomb  14662  psrval  14670  psrbasg  14678  psrelbas  14679  psrplusgg  14682  psraddcl  14684  psr0cl  14685  psrnegcl  14687  psr1clfi  14692  mplvalcoe  14694  mplplusgg  14707  toponsspwpwg  14736  topgele  14743  istps  14746  topontopn  14751  tgclb  14779  lmfval  14907  lmres  14962  ispsmet  15037  psmetge0  15045  ismet  15058  isxmet  15059  xmetge0  15079  isxms2  15166  comet  15213  bdxmet  15215  cnmetdval  15243  cnbl0  15248  cnblcld  15249  reopnap  15260  tgioo  15268  cncfcncntop  15307  cncfmpt2fcntop  15313  maxcncf  15329  mincncf  15330  hovergt0  15364  limcimolemlt  15378  cnplimcim  15381  cnplimclemr  15383  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  dvfvalap  15395  dvbss  15399  dvcnp2cntop  15413  dvcn  15414  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvrecap  15427  dvmptfsum  15439  dveflem  15440  plyval  15446  plycolemc  15472  dvply2  15481  reeff1olem  15485  pilem3  15497  ef2kpi  15520  efper  15521  sinperlem  15522  efimpi  15533  ptolemy  15538  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  cosq14gt0  15546  tangtx  15552  sinkpi  15561  coskpi  15562  cosordlem  15563  rplogcl  15593  logge0  15594  logdivlti  15595  logbleb  15675  logblt  15676  binom4  15693  wilthlem1  15694  1sgmprm  15708  1sgm2ppw  15709  mersenne  15711  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsval2lem  15729  lgsval4a  15741  lgsneg  15743  lgsdilem  15746  lgsdirprm  15753  lgsdirnn0  15766  gausslemma2dlem0i  15776  gausslemma2dlem6  15786  gausslemma2dlem7  15787  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlemofi  15795  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem2  15801  lgsquad2  15802  m1lgs  15804  2lgs  15823  2lgsoddprmlem2  15825  2lgsoddprm  15832  2sqlem2  15834  vtxvalg  15857  vtxex  15859  struct2slots2dom  15879  structvtxval  15880  structiedg0val  15881  structgrssvtx  15883  structgrssiedg  15884  edgstruct  15905  wlkv0  16166  upgr2wlkdc  16172  clwwlkex  16193  clwwlkccatlem  16195  eupthfi  16246  pwf1oexmid  16536  nnnninfex  16560  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592