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  4133  unipw  4261  opeluu  4497  uniexb  4520  unon  4559  onintrab2im  4566  xpexg  4789  resiexg  5004  imaexg  5036  exse2  5056  soirri  5077  djudisj  5110  elxp5  5171  cnvexg  5220  cnviinm  5224  coexg  5227  funssres  5313  f1oabexg  5534  sefvex  5597  ssimaex  5640  mptfvex  5665  f1ompt  5731  fmptcof  5747  resfunexg  5805  mptexg  5809  funfvima3  5818  ovid  6062  ov  6065  ofres  6173  cofunexg  6194  opabex3d  6206  opabex3  6207  oprabexd  6212  1stcof  6249  2ndcof  6250  mpoexxg  6296  cnvf1o  6311  f2ndf  6312  algrflemg  6316  tposexg  6344  tfrlemisucaccv  6411  tfrlemibxssdm  6413  tfrlemibfn  6414  tfrlemi14d  6419  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemres  6435  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemres  6448  rdgtfr  6460  rdgruledefgg  6461  rdgon  6472  frecabex  6484  freccllem  6488  frecfcllem  6490  omcl  6547  oeicl  6548  erth  6666  th3qlem1  6724  mapex  6741  pmvalg  6746  mapsnconst  6781  ixpexgg  6809  fundmen  6898  cnvct  6901  snfig  6906  unen  6908  xpdom2  6926  mapxpen  6945  phplem2  6950  findcard2  6986  findcard2s  6987  infnfi  6992  relcnvfi  7043  sbthlemi8  7066  sbthlemi10  7068  fival  7072  fiss  7079  inl11  7167  casef  7190  caseinj  7191  caseinl  7193  caseinr  7194  djudom  7195  difinfsn  7202  djuinj  7208  0ct  7209  ctmlemr  7210  ctssdccl  7213  enomnilem  7240  enmkvlem  7263  enwomnilem  7271  djuassen  7329  xpdjuen  7330  djudoml  7331  djudomr  7332  cc2lem  7378  ltnnnq  7536  nnnq0lem1  7559  addnqprlemfl  7672  addnqprlemfu  7673  mulnqprlemfl  7688  mulnqprlemfu  7689  suplocexprlem2b  7827  prsrlem1  7855  gt0srpr  7861  caucvgsrlemcl  7902  caucvgsrlemfv  7904  caucvgsrlembound  7907  mulcnsr  7948  mulcnsrec  7956  addvalex  7957  pitoregt0  7962  axmulass  7986  axdistr  7987  recriota  8003  mulrid  8069  axmulgt0  8144  cnegexlem2  8248  cnegex  8250  gt0ne0d  8585  recexre  8651  msqge0  8689  mulge0  8692  aptap  8723  recgt0  8923  recreclt  8973  cju  9034  nnge1  9059  nnnlt1  9062  nn0nlt0  9321  nnnle0  9421  elz2  9444  nnm1ge0  9459  recnz  9466  zneo  9474  uz3m2nn  9694  eluz2b2  9724  nn01to3  9738  mnflt  9905  xnn0dcle  9924  xltadd1  9998  lincmb01cmp  10125  iccf1o  10126  fz1n  10166  fseq1p1m1  10216  fznn0  10235  fzctr  10255  4fvwrd4  10262  fzo0n  10290  elfzonlteqm1  10339  divfl0  10439  modqelico  10479  zmodfz  10491  modqid  10494  modqmuladdim  10512  m1modge3gt1  10516  addmodid  10517  frec2uzf1od  10551  frecfzennn  10571  frecfzen2  10572  fzfig  10575  ser0  10678  ser3le  10682  expgt1  10722  expubnd  10741  iexpcyc  10789  binom2sub  10798  binom3  10802  zesq  10803  bernneq  10805  bernneq2  10806  expnbnd  10808  expnlbnd2  10810  facdiv  10883  faclbnd2  10887  faclbnd3  10888  bcval4  10897  hashinfom  10923  hashennn  10925  fihashf1rn  10933  isfinite4im  10937  hashfz  10966  iswrd  10996  iswrdiz  11001  wrdexg  11005  wrdexb  11006  wrdfin  11013  wrdnval  11024  wrdred1hash  11037  ccatsymb  11058  s111  11085  fzowrddc  11100  swrdlen  11105  swrdwrdsymbg  11117  crre  11168  crim  11169  remim  11171  mulreap  11175  cjreb  11177  recj  11178  reneg  11179  readd  11180  remullem  11182  imcj  11186  imneg  11187  imadd  11188  cjadd  11195  cjneg  11201  imval2  11205  cjreim  11214  cnrecnv  11221  uzin2  11298  absval  11312  rennim  11313  resqrexlemcalc3  11327  resqrexlemnm  11329  resqrexlemcvg  11330  resqrexlemgt0  11331  resqrexlemga  11334  absreimsq  11378  absreim  11379  amgm2  11429  climconst2  11602  climshft  11615  climshft2  11617  reccn2ap  11624  climge0  11636  sumsnf  11720  sumnul  11735  isumcl  11736  fsum2dlemstep  11745  fisumcom2  11749  fsumabs  11776  fsumiun  11788  binom  11795  bcxmas  11800  arisum  11809  expcnvap0  11813  explecnv  11816  geosergap  11817  geolim  11822  geolim2  11823  geo2sum  11825  geo2lim  11827  cvgratnnlemrate  11841  cvgratz  11843  mertenslemi1  11846  prodf1  11853  prodeq2w  11867  fprodntrivap  11895  prodsnf  11903  fprod2dlemstep  11933  fprodcom2fi  11937  efcllemp  11969  ege2le3  11982  eftlub  12001  efgt1  12008  tanval2ap  12024  tanval3ap  12025  resinval  12026  recosval  12027  efi4p  12028  resin4p  12029  recos4p  12030  resincl  12031  recoscl  12032  efmival  12044  efeul  12045  sinadd  12047  cosadd  12048  tanaddap  12050  sinmul  12055  cos2tsin  12062  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  sin01gt0  12073  cos01gt0  12074  absef  12081  absefib  12082  efieq1re  12083  demoivreALT  12085  eirraplem  12088  3dvds  12175  odd2np1  12184  oddm1even  12186  oddp1even  12187  oexpneg  12188  opoe  12206  omoe  12207  nn0o1gt2  12216  nn0o  12218  bitsdc  12258  bitsfzolem  12265  bitsfzo  12266  bitsinv1lem  12272  bitsinv1  12273  nninfctlemfo  12361  algcvg  12370  algcvgblem  12371  1nprm  12436  1idssfct  12437  oddprmge3  12457  divgcdodd  12465  pw2dvdslemn  12487  pw2dvds  12488  oddpwdclemodd  12494  oddpwdc  12496  phicl2  12536  phibndlem  12538  phibnd  12539  hashdvds  12543  crth  12546  phimullem  12547  eulerthlemfi  12550  eulerthlemrprm  12551  eulerthlema  12552  hashgcdeq  12562  phisum  12563  oddprm  12582  prm23ge5  12587  pythagtriplem1  12588  pythagtriplem4  12591  pythagtriplem12  12598  pythagtriplem14  12600  pczpre  12620  pcadd  12663  pcmpt  12666  pockthlem  12679  pockthi  12681  infpnlem2  12683  gzreim  12702  4sqlem11  12724  4sqlem12  12725  4sqlem13m  12726  4sqlem17  12730  2expltfac  12762  evenennn  12764  ennnfonelemjn  12773  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemnn0  12793  exmidunben  12797  ctinfomlemom  12798  ssnnctlemct  12817  nninfdc  12824  slotex  12859  setscom  12872  strslfv3  12878  setsslid  12883  basmex  12891  basmexd  12892  relelbasov  12894  ressbas2d  12900  ressbasid  12902  strressid  12903  ressval3d  12904  2strbas1g  12955  2strop1g  12956  rngbaseg  12968  rngplusgg  12969  rngmulrg  12970  srngbased  12979  srngplusgd  12980  srngmulrd  12981  srnginvld  12982  lmodbased  12997  lmodplusgd  12998  lmodscad  12999  lmodvscad  13000  ipsbased  13009  ipsaddgd  13010  ipsmulrd  13011  ipsscad  13012  ipsvscad  13013  ipsipd  13014  topgrpbasd  13029  topgrpplusgd  13030  topgrptsetd  13031  tgvalex  13095  prdsex  13101  prdsval  13105  prdsbaslemss  13106  prdsbas  13108  prdsplusg  13109  prdsmulr  13110  pwsbas  13124  pwselbasb  13125  pwssnf1o  13130  imasex  13137  imasival  13138  imasbas  13139  imasplusg  13140  imasmulr  13141  imasaddfn  13149  imasaddval  13150  imasaddf  13151  imasmulfn  13152  imasmulval  13153  imasmulf  13154  qusval  13155  qusex  13157  qusaddvallemg  13165  qusaddflemg  13166  qusaddval  13167  qusaddf  13168  qusmulval  13169  qusmulf  13170  xpsfval  13180  xpsval  13184  plusffvalg  13194  grpidvalg  13205  igsumvalx  13221  gsumfzval  13223  gsumress  13227  gsum0g  13228  gsumval2  13229  issubmnd  13274  ress0g  13275  ismhm  13293  mhmex  13294  issubm  13304  0mhm  13318  grppropstrg  13351  grpinvfvalg  13374  grpinvval  13375  grpinvfng  13376  grpsubfvalg  13377  grpsubval  13378  grpressid  13393  grplactfval  13433  qusgrp2  13449  mulgfvalg  13457  mulgex  13459  mulgnngsum  13463  issubg  13509  subgex  13512  subgmulg  13524  issubg2m  13525  releqgg  13556  eqgex  13557  eqgfval  13558  eqgen  13563  isghm  13579  ablressid  13671  mgptopng  13691  rngressid  13716  qusrng  13720  dfur2g  13724  ringidss  13791  ring1  13821  ringressid  13825  qusring2  13828  reldvdsrsrg  13854  dvdsrvald  13855  dvdsrex  13860  unitgrp  13878  unitabl  13879  invrfvald  13884  unitlinv  13888  unitrinv  13889  dvrfvald  13895  rdivmuldivd  13906  invrpropdg  13911  rhmunitinv  13940  isnzr2  13946  issubrng  13961  issubrg  13983  subrgugrp  14002  subrgpropd  14015  rrgmex  14023  aprval  14044  islmod  14053  scaffvalg  14068  lssex  14116  lssmex  14117  lsssetm  14118  islssmg  14120  islss3  14141  lspfval  14150  lspval  14152  lspcl  14153  lspex  14157  sralemg  14200  srascag  14204  sravscag  14205  sraipg  14206  sraex  14208  rlmsubg  14220  rlmvnegg  14227  ixpsnbasval  14228  lidlvalg  14233  rspvalg  14234  lidlex  14235  rspex  14236  lidlmex  14237  lidlss  14238  lidlrsppropdg  14257  2idlmex  14263  qusrhm  14290  znlidl  14396  zncrng2  14397  znval  14398  znle  14399  znbaslemnn  14401  znbas  14406  znzrh2  14408  znzrhval  14409  znzrhfo  14410  zndvds  14411  znfi  14417  znhash  14418  znidom  14419  znidomb  14420  psrval  14428  psrbasg  14436  psrelbas  14437  psrplusgg  14440  psraddcl  14442  psr0cl  14443  psrnegcl  14445  psr1clfi  14450  mplvalcoe  14452  mplplusgg  14465  toponsspwpwg  14494  topgele  14501  istps  14504  topontopn  14509  tgclb  14537  lmfval  14664  lmres  14720  ispsmet  14795  psmetge0  14803  ismet  14816  isxmet  14817  xmetge0  14837  isxms2  14924  comet  14971  bdxmet  14973  cnmetdval  15001  cnbl0  15006  cnblcld  15007  reopnap  15018  tgioo  15026  cncfcncntop  15065  cncfmpt2fcntop  15071  maxcncf  15087  mincncf  15088  hovergt0  15122  limcimolemlt  15136  cnplimcim  15139  cnplimclemr  15141  limccnpcntop  15147  limccnp2lem  15148  limccnp2cntop  15149  dvfvalap  15153  dvbss  15157  dvcnp2cntop  15171  dvcn  15172  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvrecap  15185  dvmptfsum  15197  dveflem  15198  plyval  15204  plycolemc  15230  dvply2  15239  reeff1olem  15243  pilem3  15255  ef2kpi  15278  efper  15279  sinperlem  15280  efimpi  15291  ptolemy  15296  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  sinq12gt0  15302  cosq14gt0  15304  tangtx  15310  sinkpi  15319  coskpi  15320  cosordlem  15321  rplogcl  15351  logge0  15352  logdivlti  15353  logbleb  15433  logblt  15434  binom4  15451  wilthlem1  15452  1sgmprm  15466  1sgm2ppw  15467  mersenne  15469  perfect1  15470  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgsval2lem  15487  lgsval4a  15499  lgsneg  15501  lgsdilem  15504  lgsdirprm  15511  lgsdirnn0  15524  gausslemma2dlem0i  15534  gausslemma2dlem6  15544  gausslemma2dlem7  15545  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlemofi  15553  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem2  15559  lgsquad2  15560  m1lgs  15562  2lgs  15581  2lgsoddprmlem2  15583  2lgsoddprm  15590  2sqlem2  15592  vtxvalg  15615  struct2slots2dom  15635  structvtxval  15636  structiedg0val  15637  structgrssvtx  15639  structgrssiedg  15640  edgstruct  15656  pwf1oexmid  15936  nnnninfex  15959  isomninnlem  15969  iswomninnlem  15988  ismkvnnlem  15991