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  7302  xpdjuen  7303  djudoml  7304  djudomr  7305  cc2lem  7351  ltnnnq  7509  nnnq0lem1  7532  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemfl  7661  mulnqprlemfu  7662  suplocexprlem2b  7800  prsrlem1  7828  gt0srpr  7834  caucvgsrlemcl  7875  caucvgsrlemfv  7877  caucvgsrlembound  7880  mulcnsr  7921  mulcnsrec  7929  addvalex  7930  pitoregt0  7935  axmulass  7959  axdistr  7960  recriota  7976  mulrid  8042  axmulgt0  8117  cnegexlem2  8221  cnegex  8223  gt0ne0d  8558  recexre  8624  msqge0  8662  mulge0  8665  aptap  8696  recgt0  8896  recreclt  8946  cju  9007  nnge1  9032  nnnlt1  9035  nn0nlt0  9294  elz2  9416  nnm1ge0  9431  recnz  9438  zneo  9446  uz3m2nn  9666  eluz2b2  9696  nn01to3  9710  mnflt  9877  xnn0dcle  9896  xltadd1  9970  lincmb01cmp  10097  iccf1o  10098  fz1n  10138  fseq1p1m1  10188  fznn0  10207  fzctr  10227  4fvwrd4  10234  elfzonlteqm1  10305  divfl0  10405  modqelico  10445  zmodfz  10457  modqid  10460  modqmuladdim  10478  m1modge3gt1  10482  addmodid  10483  frec2uzf1od  10517  frecfzennn  10537  frecfzen2  10538  fzfig  10541  ser0  10644  ser3le  10648  expgt1  10688  expubnd  10707  iexpcyc  10755  binom2sub  10764  binom3  10768  zesq  10769  bernneq  10771  bernneq2  10772  expnbnd  10774  expnlbnd2  10776  facdiv  10849  faclbnd2  10853  faclbnd3  10854  bcval4  10863  hashinfom  10889  hashennn  10891  fihashf1rn  10899  isfinite4im  10903  hashfz  10932  iswrd  10956  iswrdiz  10961  wrdexg  10965  wrdexb  10966  wrdfin  10973  wrdnval  10984  wrdred1hash  10997  crre  11041  crim  11042  remim  11044  mulreap  11048  cjreb  11050  recj  11051  reneg  11052  readd  11053  remullem  11055  imcj  11059  imneg  11060  imadd  11061  cjadd  11068  cjneg  11074  imval2  11078  cjreim  11087  cnrecnv  11094  uzin2  11171  absval  11185  rennim  11186  resqrexlemcalc3  11200  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemgt0  11204  resqrexlemga  11207  absreimsq  11251  absreim  11252  amgm2  11302  climconst2  11475  climshft  11488  climshft2  11490  reccn2ap  11497  climge0  11509  sumsnf  11593  sumnul  11608  isumcl  11609  fsum2dlemstep  11618  fisumcom2  11622  fsumabs  11649  fsumiun  11661  binom  11668  bcxmas  11673  arisum  11682  expcnvap0  11686  explecnv  11689  geosergap  11690  geolim  11695  geolim2  11696  geo2sum  11698  geo2lim  11700  cvgratnnlemrate  11714  cvgratz  11716  mertenslemi1  11719  prodf1  11726  prodeq2w  11740  fprodntrivap  11768  prodsnf  11776  fprod2dlemstep  11806  fprodcom2fi  11810  efcllemp  11842  ege2le3  11855  eftlub  11874  efgt1  11881  tanval2ap  11897  tanval3ap  11898  resinval  11899  recosval  11900  efi4p  11901  resin4p  11902  recos4p  11903  resincl  11904  recoscl  11905  efmival  11917  efeul  11918  sinadd  11920  cosadd  11921  tanaddap  11923  sinmul  11928  cos2tsin  11935  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  cos01gt0  11947  absef  11954  absefib  11955  efieq1re  11956  demoivreALT  11958  eirraplem  11961  3dvds  12048  odd2np1  12057  oddm1even  12059  oddp1even  12060  oexpneg  12061  opoe  12079  omoe  12080  nn0o1gt2  12089  nn0o  12091  bitsdc  12131  bitsfzolem  12138  bitsfzo  12139  bitsinv1lem  12145  bitsinv1  12146  nninfctlemfo  12234  algcvg  12243  algcvgblem  12244  1nprm  12309  1idssfct  12310  oddprmge3  12330  divgcdodd  12338  pw2dvdslemn  12360  pw2dvds  12361  oddpwdclemodd  12367  oddpwdc  12369  phicl2  12409  phibndlem  12411  phibnd  12412  hashdvds  12416  crth  12419  phimullem  12420  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlema  12425  hashgcdeq  12435  phisum  12436  oddprm  12455  prm23ge5  12460  pythagtriplem1  12461  pythagtriplem4  12464  pythagtriplem12  12471  pythagtriplem14  12473  pczpre  12493  pcadd  12536  pcmpt  12539  pockthlem  12552  pockthi  12554  infpnlem2  12556  gzreim  12575  4sqlem11  12597  4sqlem12  12598  4sqlem13m  12599  4sqlem17  12603  2expltfac  12635  evenennn  12637  ennnfonelemjn  12646  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemnn0  12666  exmidunben  12670  ctinfomlemom  12671  ssnnctlemct  12690  nninfdc  12697  slotex  12732  setscom  12745  strslfv3  12751  setsslid  12756  basmex  12764  basmexd  12765  relelbasov  12767  ressbas2d  12773  ressbasid  12775  strressid  12776  ressval3d  12777  2strbas1g  12827  2strop1g  12828  rngbaseg  12840  rngplusgg  12841  rngmulrg  12842  srngbased  12851  srngplusgd  12852  srngmulrd  12853  srnginvld  12854  lmodbased  12869  lmodplusgd  12870  lmodscad  12871  lmodvscad  12872  ipsbased  12881  ipsaddgd  12882  ipsmulrd  12883  ipsscad  12884  ipsvscad  12885  ipsipd  12886  topgrpbasd  12901  topgrpplusgd  12902  topgrptsetd  12903  tgvalex  12967  prdsex  12973  prdsval  12977  prdsbaslemss  12978  prdsbas  12980  prdsplusg  12981  prdsmulr  12982  pwsbas  12996  pwselbasb  12997  pwssnf1o  13002  imasex  13009  imasival  13010  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfn  13021  imasaddval  13022  imasaddf  13023  imasmulfn  13024  imasmulval  13025  imasmulf  13026  qusval  13027  qusex  13029  qusaddvallemg  13037  qusaddflemg  13038  qusaddval  13039  qusaddf  13040  qusmulval  13041  qusmulf  13042  xpsfval  13052  xpsval  13056  plusffvalg  13066  grpidvalg  13077  igsumvalx  13093  gsumfzval  13095  gsumress  13099  gsum0g  13100  gsumval2  13101  issubmnd  13146  ress0g  13147  ismhm  13165  mhmex  13166  issubm  13176  0mhm  13190  grppropstrg  13223  grpinvfvalg  13246  grpinvval  13247  grpinvfng  13248  grpsubfvalg  13249  grpsubval  13250  grpressid  13265  grplactfval  13305  qusgrp2  13321  mulgfvalg  13329  mulgex  13331  mulgnngsum  13335  issubg  13381  subgex  13384  subgmulg  13396  issubg2m  13397  releqgg  13428  eqgex  13429  eqgfval  13430  eqgen  13435  isghm  13451  ablressid  13543  mgptopng  13563  rngressid  13588  qusrng  13592  dfur2g  13596  ringidss  13663  ring1  13693  ringressid  13697  qusring2  13700  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrex  13732  unitgrp  13750  unitabl  13751  invrfvald  13756  unitlinv  13760  unitrinv  13761  dvrfvald  13767  rdivmuldivd  13778  invrpropdg  13783  rhmunitinv  13812  isnzr2  13818  issubrng  13833  issubrg  13855  subrgugrp  13874  subrgpropd  13887  rrgmex  13895  aprval  13916  islmod  13925  scaffvalg  13940  lssex  13988  lssmex  13989  lsssetm  13990  islssmg  13992  islss3  14013  lspfval  14022  lspval  14024  lspcl  14025  lspex  14029  sralemg  14072  srascag  14076  sravscag  14077  sraipg  14078  sraex  14080  rlmsubg  14092  rlmvnegg  14099  ixpsnbasval  14100  lidlvalg  14105  rspvalg  14106  lidlex  14107  rspex  14108  lidlmex  14109  lidlss  14110  lidlrsppropdg  14129  2idlmex  14135  qusrhm  14162  znlidl  14268  zncrng2  14269  znval  14270  znle  14271  znbaslemnn  14273  znbas  14278  znzrh2  14280  znzrhval  14281  znzrhfo  14282  zndvds  14283  znfi  14289  znhash  14290  znidom  14291  znidomb  14292  psrval  14300  psrbasg  14308  psrelbas  14309  psrplusgg  14312  psraddcl  14314  psr0cl  14315  psrnegcl  14317  psr1clfi  14322  mplvalcoe  14324  mplplusgg  14337  toponsspwpwg  14366  topgele  14373  istps  14376  topontopn  14381  tgclb  14409  lmfval  14536  lmres  14592  ispsmet  14667  psmetge0  14675  ismet  14688  isxmet  14689  xmetge0  14709  isxms2  14796  comet  14843  bdxmet  14845  cnmetdval  14873  cnbl0  14878  cnblcld  14879  reopnap  14890  tgioo  14898  cncfcncntop  14937  cncfmpt2fcntop  14943  maxcncf  14959  mincncf  14960  hovergt0  14994  limcimolemlt  15008  cnplimcim  15011  cnplimclemr  15013  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  dvfvalap  15025  dvbss  15029  dvcnp2cntop  15043  dvcn  15044  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvrecap  15057  dvmptfsum  15069  dveflem  15070  plyval  15076  plycolemc  15102  dvply2  15111  reeff1olem  15115  pilem3  15127  ef2kpi  15150  efper  15151  sinperlem  15152  efimpi  15163  ptolemy  15168  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  sinq12gt0  15174  cosq14gt0  15176  tangtx  15182  sinkpi  15191  coskpi  15192  cosordlem  15193  rplogcl  15223  logge0  15224  logdivlti  15225  logbleb  15305  logblt  15306  binom4  15323  wilthlem1  15324  1sgmprm  15338  1sgm2ppw  15339  mersenne  15341  perfect1  15342  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgsval2lem  15359  lgsval4a  15371  lgsneg  15373  lgsdilem  15376  lgsdirprm  15383  lgsdirnn0  15396  gausslemma2dlem0i  15406  gausslemma2dlem6  15416  gausslemma2dlem7  15417  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlemofi  15425  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem2  15431  lgsquad2  15432  m1lgs  15434  2lgs  15453  2lgsoddprmlem2  15455  2lgsoddprm  15462  2sqlem2  15464  pwf1oexmid  15754  nnnninfex  15777  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809