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  4149  unipw  4279  opeluu  4515  uniexb  4538  unon  4577  onintrab2im  4584  xpexg  4807  resiexg  5023  imaexg  5055  exse2  5075  soirri  5096  djudisj  5129  elxp5  5190  cnvexg  5239  cnviinm  5243  coexg  5246  funssres  5332  f1oabexg  5556  sefvex  5620  ssimaex  5663  mptfvex  5688  f1ompt  5754  fmptcof  5770  resfunexg  5828  mptexg  5832  funfvima3  5841  ovid  6085  ov  6088  ofres  6196  cofunexg  6217  opabex3d  6229  opabex3  6230  oprabexd  6235  1stcof  6272  2ndcof  6273  mpoexxg  6319  cnvf1o  6334  f2ndf  6335  algrflemg  6339  tposexg  6367  tfrlemisucaccv  6434  tfrlemibxssdm  6436  tfrlemibfn  6437  tfrlemi14d  6442  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemres  6458  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemres  6471  rdgtfr  6483  rdgruledefgg  6484  rdgon  6495  frecabex  6507  freccllem  6511  frecfcllem  6513  omcl  6570  oeicl  6571  erth  6689  th3qlem1  6747  mapex  6764  pmvalg  6769  mapsnconst  6804  ixpexgg  6832  fundmen  6922  cnvct  6925  snfig  6930  unen  6932  xpdom2  6951  mapxpen  6970  phplem2  6975  findcard2  7012  findcard2s  7013  infnfi  7018  relcnvfi  7069  sbthlemi8  7092  sbthlemi10  7094  fival  7098  fiss  7105  inl11  7193  casef  7216  caseinj  7217  caseinl  7219  caseinr  7220  djudom  7221  difinfsn  7228  djuinj  7234  0ct  7235  ctmlemr  7236  ctssdccl  7239  enomnilem  7266  enmkvlem  7289  enwomnilem  7297  djuassen  7360  xpdjuen  7361  djudoml  7362  djudomr  7363  cc2lem  7413  ltnnnq  7571  nnnq0lem1  7594  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemfl  7723  mulnqprlemfu  7724  suplocexprlem2b  7862  prsrlem1  7890  gt0srpr  7896  caucvgsrlemcl  7937  caucvgsrlemfv  7939  caucvgsrlembound  7942  mulcnsr  7983  mulcnsrec  7991  addvalex  7992  pitoregt0  7997  axmulass  8021  axdistr  8022  recriota  8038  mulrid  8104  axmulgt0  8179  cnegexlem2  8283  cnegex  8285  gt0ne0d  8620  recexre  8686  msqge0  8724  mulge0  8727  aptap  8758  recgt0  8958  recreclt  9008  cju  9069  nnge1  9094  nnnlt1  9097  nn0nlt0  9356  nnnle0  9456  elz2  9479  nnm1ge0  9494  recnz  9501  zneo  9509  uz3m2nn  9729  eluz2b2  9759  nn01to3  9773  mnflt  9940  xnn0dcle  9959  xltadd1  10033  lincmb01cmp  10160  iccf1o  10161  fz1n  10201  fseq1p1m1  10251  fznn0  10270  fzctr  10290  4fvwrd4  10297  fzo0n  10325  elfzonlteqm1  10376  divfl0  10476  modqelico  10516  zmodfz  10528  modqid  10531  modqmuladdim  10549  m1modge3gt1  10553  addmodid  10554  frec2uzf1od  10588  frecfzennn  10608  frecfzen2  10609  fzfig  10612  ser0  10715  ser3le  10719  expgt1  10759  expubnd  10778  iexpcyc  10826  binom2sub  10835  binom3  10839  zesq  10840  bernneq  10842  bernneq2  10843  expnbnd  10845  expnlbnd2  10847  facdiv  10920  faclbnd2  10924  faclbnd3  10925  bcval4  10934  hashinfom  10960  hashennn  10962  fihashf1rn  10970  isfinite4im  10974  hashfz  11003  iswrd  11033  iswrdiz  11038  wrdexg  11042  wrdexb  11043  wrdfin  11050  wrdnval  11061  wrdred1hash  11074  ccatsymb  11096  s111  11123  fzowrddc  11138  swrdlen  11143  swrdwrdsymbg  11155  pfxval  11165  pfx0g  11167  fnpfx  11168  pfxlen  11176  cats1un  11212  swrdccat  11226  crre  11283  crim  11284  remim  11286  mulreap  11290  cjreb  11292  recj  11293  reneg  11294  readd  11295  remullem  11297  imcj  11301  imneg  11302  imadd  11303  cjadd  11310  cjneg  11316  imval2  11320  cjreim  11329  cnrecnv  11336  uzin2  11413  absval  11427  rennim  11428  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemgt0  11446  resqrexlemga  11449  absreimsq  11493  absreim  11494  amgm2  11544  climconst2  11717  climshft  11730  climshft2  11732  reccn2ap  11739  climge0  11751  sumsnf  11835  sumnul  11850  isumcl  11851  fsum2dlemstep  11860  fisumcom2  11864  fsumabs  11891  fsumiun  11903  binom  11910  bcxmas  11915  arisum  11924  expcnvap0  11928  explecnv  11931  geosergap  11932  geolim  11937  geolim2  11938  geo2sum  11940  geo2lim  11942  cvgratnnlemrate  11956  cvgratz  11958  mertenslemi1  11961  prodf1  11968  prodeq2w  11982  fprodntrivap  12010  prodsnf  12018  fprod2dlemstep  12048  fprodcom2fi  12052  efcllemp  12084  ege2le3  12097  eftlub  12116  efgt1  12123  tanval2ap  12139  tanval3ap  12140  resinval  12141  recosval  12142  efi4p  12143  resin4p  12144  recos4p  12145  resincl  12146  recoscl  12147  efmival  12159  efeul  12160  sinadd  12162  cosadd  12163  tanaddap  12165  sinmul  12170  cos2tsin  12177  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  sin01gt0  12188  cos01gt0  12189  absef  12196  absefib  12197  efieq1re  12198  demoivreALT  12200  eirraplem  12203  3dvds  12290  odd2np1  12299  oddm1even  12301  oddp1even  12302  oexpneg  12303  opoe  12321  omoe  12322  nn0o1gt2  12331  nn0o  12333  bitsdc  12373  bitsfzolem  12380  bitsfzo  12381  bitsinv1lem  12387  bitsinv1  12388  nninfctlemfo  12476  algcvg  12485  algcvgblem  12486  1nprm  12551  1idssfct  12552  oddprmge3  12572  divgcdodd  12580  pw2dvdslemn  12602  pw2dvds  12603  oddpwdclemodd  12609  oddpwdc  12611  phicl2  12651  phibndlem  12653  phibnd  12654  hashdvds  12658  crth  12661  phimullem  12662  eulerthlemfi  12665  eulerthlemrprm  12666  eulerthlema  12667  hashgcdeq  12677  phisum  12678  oddprm  12697  prm23ge5  12702  pythagtriplem1  12703  pythagtriplem4  12706  pythagtriplem12  12713  pythagtriplem14  12715  pczpre  12735  pcadd  12778  pcmpt  12781  pockthlem  12794  pockthi  12796  infpnlem2  12798  gzreim  12817  4sqlem11  12839  4sqlem12  12840  4sqlem13m  12841  4sqlem17  12845  2expltfac  12877  evenennn  12879  ennnfonelemjn  12888  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemnn0  12908  exmidunben  12912  ctinfomlemom  12913  ssnnctlemct  12932  nninfdc  12939  slotex  12974  setscom  12987  strslfv3  12993  setsslid  12998  basmex  13006  basmexd  13007  relelbasov  13009  ressbas2d  13015  ressbasid  13017  strressid  13018  ressval3d  13019  2strbas1g  13070  2strop1g  13071  rngbaseg  13083  rngplusgg  13084  rngmulrg  13085  srngbased  13094  srngplusgd  13095  srngmulrd  13096  srnginvld  13097  lmodbased  13112  lmodplusgd  13113  lmodscad  13114  lmodvscad  13115  ipsbased  13124  ipsaddgd  13125  ipsmulrd  13126  ipsscad  13127  ipsvscad  13128  ipsipd  13129  topgrpbasd  13144  topgrpplusgd  13145  topgrptsetd  13146  tgvalex  13210  prdsex  13216  prdsval  13220  prdsbaslemss  13221  prdsbas  13223  prdsplusg  13224  prdsmulr  13225  pwsbas  13239  pwselbasb  13240  pwssnf1o  13245  imasex  13252  imasival  13253  imasbas  13254  imasplusg  13255  imasmulr  13256  imasaddfn  13264  imasaddval  13265  imasaddf  13266  imasmulfn  13267  imasmulval  13268  imasmulf  13269  qusval  13270  qusex  13272  qusaddvallemg  13280  qusaddflemg  13281  qusaddval  13282  qusaddf  13283  qusmulval  13284  qusmulf  13285  xpsfval  13295  xpsval  13299  plusffvalg  13309  grpidvalg  13320  igsumvalx  13336  gsumfzval  13338  gsumress  13342  gsum0g  13343  gsumval2  13344  issubmnd  13389  ress0g  13390  ismhm  13408  mhmex  13409  issubm  13419  0mhm  13433  grppropstrg  13466  grpinvfvalg  13489  grpinvval  13490  grpinvfng  13491  grpsubfvalg  13492  grpsubval  13493  grpressid  13508  grplactfval  13548  qusgrp2  13564  mulgfvalg  13572  mulgex  13574  mulgnngsum  13578  issubg  13624  subgex  13627  subgmulg  13639  issubg2m  13640  releqgg  13671  eqgex  13672  eqgfval  13673  eqgen  13678  isghm  13694  ablressid  13786  mgptopng  13806  rngressid  13831  qusrng  13835  dfur2g  13839  ringidss  13906  ring1  13936  ringressid  13940  qusring2  13943  reldvdsrsrg  13969  dvdsrvald  13970  dvdsrex  13975  unitgrp  13993  unitabl  13994  invrfvald  13999  unitlinv  14003  unitrinv  14004  dvrfvald  14010  rdivmuldivd  14021  invrpropdg  14026  rhmunitinv  14055  isnzr2  14061  issubrng  14076  issubrg  14098  subrgugrp  14117  subrgpropd  14130  rrgmex  14138  aprval  14159  islmod  14168  scaffvalg  14183  lssex  14231  lssmex  14232  lsssetm  14233  islssmg  14235  islss3  14256  lspfval  14265  lspval  14267  lspcl  14268  lspex  14272  sralemg  14315  srascag  14319  sravscag  14320  sraipg  14321  sraex  14323  rlmsubg  14335  rlmvnegg  14342  ixpsnbasval  14343  lidlvalg  14348  rspvalg  14349  lidlex  14350  rspex  14351  lidlmex  14352  lidlss  14353  lidlrsppropdg  14372  2idlmex  14378  qusrhm  14405  znlidl  14511  zncrng2  14512  znval  14513  znle  14514  znbaslemnn  14516  znbas  14521  znzrh2  14523  znzrhval  14524  znzrhfo  14525  zndvds  14526  znfi  14532  znhash  14533  znidom  14534  znidomb  14535  psrval  14543  psrbasg  14551  psrelbas  14552  psrplusgg  14555  psraddcl  14557  psr0cl  14558  psrnegcl  14560  psr1clfi  14565  mplvalcoe  14567  mplplusgg  14580  toponsspwpwg  14609  topgele  14616  istps  14619  topontopn  14624  tgclb  14652  lmfval  14779  lmres  14835  ispsmet  14910  psmetge0  14918  ismet  14931  isxmet  14932  xmetge0  14952  isxms2  15039  comet  15086  bdxmet  15088  cnmetdval  15116  cnbl0  15121  cnblcld  15122  reopnap  15133  tgioo  15141  cncfcncntop  15180  cncfmpt2fcntop  15186  maxcncf  15202  mincncf  15203  hovergt0  15237  limcimolemlt  15251  cnplimcim  15254  cnplimclemr  15256  limccnpcntop  15262  limccnp2lem  15263  limccnp2cntop  15264  dvfvalap  15268  dvbss  15272  dvcnp2cntop  15286  dvcn  15287  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvcjbr  15295  dvrecap  15300  dvmptfsum  15312  dveflem  15313  plyval  15319  plycolemc  15345  dvply2  15354  reeff1olem  15358  pilem3  15370  ef2kpi  15393  efper  15394  sinperlem  15395  efimpi  15406  ptolemy  15411  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  sinq12gt0  15417  cosq14gt0  15419  tangtx  15425  sinkpi  15434  coskpi  15435  cosordlem  15436  rplogcl  15466  logge0  15467  logdivlti  15468  logbleb  15548  logblt  15549  binom4  15566  wilthlem1  15567  1sgmprm  15581  1sgm2ppw  15582  mersenne  15584  perfect1  15585  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgsval2lem  15602  lgsval4a  15614  lgsneg  15616  lgsdilem  15619  lgsdirprm  15626  lgsdirnn0  15639  gausslemma2dlem0i  15649  gausslemma2dlem6  15659  gausslemma2dlem7  15660  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlemofi  15668  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem2  15674  lgsquad2  15675  m1lgs  15677  2lgs  15696  2lgsoddprmlem2  15698  2lgsoddprm  15705  2sqlem2  15707  vtxvalg  15730  vtxex  15732  struct2slots2dom  15752  structvtxval  15753  structiedg0val  15754  structgrssvtx  15756  structgrssiedg  15757  edgstruct  15775  pwf1oexmid  16138  nnnninfex  16161  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193