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  4122  unipw  4250  opeluu  4485  uniexb  4508  unon  4547  onintrab2im  4554  xpexg  4777  resiexg  4991  imaexg  5023  exse2  5043  soirri  5064  djudisj  5097  elxp5  5158  cnvexg  5207  cnviinm  5211  coexg  5214  funssres  5300  f1oabexg  5516  sefvex  5579  ssimaex  5622  mptfvex  5647  f1ompt  5713  fmptcof  5729  resfunexg  5783  mptexg  5787  funfvima3  5796  ovid  6039  ov  6042  ofres  6150  cofunexg  6166  opabex3d  6178  opabex3  6179  oprabexd  6184  1stcof  6221  2ndcof  6222  mpoexxg  6268  cnvf1o  6283  f2ndf  6284  algrflemg  6288  tposexg  6316  tfrlemisucaccv  6383  tfrlemibxssdm  6385  tfrlemibfn  6386  tfrlemi14d  6391  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemres  6407  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemres  6420  rdgtfr  6432  rdgruledefgg  6433  rdgon  6444  frecabex  6456  freccllem  6460  frecfcllem  6462  omcl  6519  oeicl  6520  erth  6638  th3qlem1  6696  mapex  6713  pmvalg  6718  mapsnconst  6753  ixpexgg  6781  fundmen  6865  cnvct  6868  snfig  6873  unen  6875  xpdom2  6890  mapxpen  6909  phplem2  6914  findcard2  6950  findcard2s  6951  infnfi  6956  relcnvfi  7007  sbthlemi8  7030  sbthlemi10  7032  fival  7036  fiss  7043  inl11  7131  casef  7154  caseinj  7155  caseinl  7157  caseinr  7158  djudom  7159  difinfsn  7166  djuinj  7172  0ct  7173  ctmlemr  7174  ctssdccl  7177  enomnilem  7204  enmkvlem  7227  enwomnilem  7235  djuassen  7284  xpdjuen  7285  djudoml  7286  djudomr  7287  cc2lem  7333  ltnnnq  7490  nnnq0lem1  7513  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemfl  7642  mulnqprlemfu  7643  suplocexprlem2b  7781  prsrlem1  7809  gt0srpr  7815  caucvgsrlemcl  7856  caucvgsrlemfv  7858  caucvgsrlembound  7861  mulcnsr  7902  mulcnsrec  7910  addvalex  7911  pitoregt0  7916  axmulass  7940  axdistr  7941  recriota  7957  mulrid  8023  axmulgt0  8098  cnegexlem2  8202  cnegex  8204  gt0ne0d  8539  recexre  8605  msqge0  8643  mulge0  8646  aptap  8677  recgt0  8877  recreclt  8927  cju  8988  nnge1  9013  nnnlt1  9016  nn0nlt0  9275  elz2  9397  nnm1ge0  9412  recnz  9419  zneo  9427  uz3m2nn  9647  eluz2b2  9677  nn01to3  9691  mnflt  9858  xnn0dcle  9877  xltadd1  9951  lincmb01cmp  10078  iccf1o  10079  fz1n  10119  fseq1p1m1  10169  fznn0  10188  fzctr  10208  4fvwrd4  10215  elfzonlteqm1  10286  divfl0  10386  modqelico  10426  zmodfz  10438  modqid  10441  modqmuladdim  10459  m1modge3gt1  10463  addmodid  10464  frec2uzf1od  10498  frecfzennn  10518  frecfzen2  10519  fzfig  10522  ser0  10625  ser3le  10629  expgt1  10669  expubnd  10688  iexpcyc  10736  binom2sub  10745  binom3  10749  zesq  10750  bernneq  10752  bernneq2  10753  expnbnd  10755  expnlbnd2  10757  facdiv  10830  faclbnd2  10834  faclbnd3  10835  bcval4  10844  hashinfom  10870  hashennn  10872  fihashf1rn  10880  isfinite4im  10884  hashfz  10913  iswrd  10937  iswrdiz  10942  wrdexg  10946  wrdexb  10947  wrdfin  10954  wrdnval  10965  wrdred1hash  10978  crre  11022  crim  11023  remim  11025  mulreap  11029  cjreb  11031  recj  11032  reneg  11033  readd  11034  remullem  11036  imcj  11040  imneg  11041  imadd  11042  cjadd  11049  cjneg  11055  imval2  11059  cjreim  11068  cnrecnv  11075  uzin2  11152  absval  11166  rennim  11167  resqrexlemcalc3  11181  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemgt0  11185  resqrexlemga  11188  absreimsq  11232  absreim  11233  amgm2  11283  climconst2  11456  climshft  11469  climshft2  11471  reccn2ap  11478  climge0  11490  sumsnf  11574  sumnul  11589  isumcl  11590  fsum2dlemstep  11599  fisumcom2  11603  fsumabs  11630  fsumiun  11642  binom  11649  bcxmas  11654  arisum  11663  expcnvap0  11667  explecnv  11670  geosergap  11671  geolim  11676  geolim2  11677  geo2sum  11679  geo2lim  11681  cvgratnnlemrate  11695  cvgratz  11697  mertenslemi1  11700  prodf1  11707  prodeq2w  11721  fprodntrivap  11749  prodsnf  11757  fprod2dlemstep  11787  fprodcom2fi  11791  efcllemp  11823  ege2le3  11836  eftlub  11855  efgt1  11862  tanval2ap  11878  tanval3ap  11879  resinval  11880  recosval  11881  efi4p  11882  resin4p  11883  recos4p  11884  resincl  11885  recoscl  11886  efmival  11898  efeul  11899  sinadd  11901  cosadd  11902  tanaddap  11904  sinmul  11909  cos2tsin  11916  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  sin01gt0  11927  cos01gt0  11928  absef  11935  absefib  11936  efieq1re  11937  demoivreALT  11939  eirraplem  11942  3dvds  12029  odd2np1  12038  oddm1even  12040  oddp1even  12041  oexpneg  12042  opoe  12060  omoe  12061  nn0o1gt2  12070  nn0o  12072  bitsfzolem  12118  bitsfzo  12119  nninfctlemfo  12207  algcvg  12216  algcvgblem  12217  1nprm  12282  1idssfct  12283  oddprmge3  12303  divgcdodd  12311  pw2dvdslemn  12333  pw2dvds  12334  oddpwdclemodd  12340  oddpwdc  12342  phicl2  12382  phibndlem  12384  phibnd  12385  hashdvds  12389  crth  12392  phimullem  12393  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlema  12398  hashgcdeq  12408  phisum  12409  oddprm  12428  prm23ge5  12433  pythagtriplem1  12434  pythagtriplem4  12437  pythagtriplem12  12444  pythagtriplem14  12446  pczpre  12466  pcadd  12509  pcmpt  12512  pockthlem  12525  pockthi  12527  infpnlem2  12529  gzreim  12548  4sqlem11  12570  4sqlem12  12571  4sqlem13m  12572  4sqlem17  12576  2expltfac  12608  evenennn  12610  ennnfonelemjn  12619  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemnn0  12639  exmidunben  12643  ctinfomlemom  12644  ssnnctlemct  12663  nninfdc  12670  slotex  12705  setscom  12718  setsslid  12729  basmex  12737  basmexd  12738  relelbasov  12740  ressbas2d  12746  ressbasid  12748  strressid  12749  ressval3d  12750  2strbas1g  12800  2strop1g  12801  rngbaseg  12813  rngplusgg  12814  rngmulrg  12815  srngbased  12824  srngplusgd  12825  srngmulrd  12826  srnginvld  12827  lmodbased  12842  lmodplusgd  12843  lmodscad  12844  lmodvscad  12845  ipsbased  12854  ipsaddgd  12855  ipsmulrd  12856  ipsscad  12857  ipsvscad  12858  ipsipd  12859  topgrpbasd  12874  topgrpplusgd  12875  topgrptsetd  12876  tgvalex  12934  prdsex  12940  imasex  12948  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfn  12960  imasaddval  12961  imasaddf  12962  imasmulfn  12963  imasmulval  12964  imasmulf  12965  qusval  12966  qusex  12968  qusaddvallemg  12976  qusaddflemg  12977  qusaddval  12978  qusaddf  12979  qusmulval  12980  qusmulf  12981  xpsfval  12991  xpsval  12995  plusffvalg  13005  grpidvalg  13016  igsumvalx  13032  gsumfzval  13034  gsumress  13038  gsum0g  13039  gsumval2  13040  issubmnd  13083  ress0g  13084  ismhm  13093  mhmex  13094  issubm  13104  0mhm  13118  grppropstrg  13151  grpinvfvalg  13174  grpinvval  13175  grpinvfng  13176  grpsubfvalg  13177  grpsubval  13178  grpressid  13193  grplactfval  13233  qusgrp2  13243  mulgfvalg  13251  mulgex  13253  mulgnngsum  13257  issubg  13303  subgex  13306  subgmulg  13318  issubg2m  13319  releqgg  13350  eqgex  13351  eqgfval  13352  eqgen  13357  isghm  13373  ablressid  13465  mgptopng  13485  rngressid  13510  qusrng  13514  dfur2g  13518  ringidss  13585  ring1  13615  ringressid  13619  qusring2  13622  reldvdsrsrg  13648  dvdsrvald  13649  dvdsrex  13654  unitgrp  13672  unitabl  13673  invrfvald  13678  unitlinv  13682  unitrinv  13683  dvrfvald  13689  rdivmuldivd  13700  invrpropdg  13705  rhmunitinv  13734  isnzr2  13740  issubrng  13755  issubrg  13777  subrgugrp  13796  subrgpropd  13809  rrgmex  13817  aprval  13838  islmod  13847  scaffvalg  13862  lssex  13910  lssmex  13911  lsssetm  13912  islssmg  13914  islss3  13935  lspfval  13944  lspval  13946  lspcl  13947  lspex  13951  sralemg  13994  srascag  13998  sravscag  13999  sraipg  14000  sraex  14002  rlmsubg  14014  rlmvnegg  14021  ixpsnbasval  14022  lidlvalg  14027  rspvalg  14028  lidlex  14029  rspex  14030  lidlmex  14031  lidlss  14032  lidlrsppropdg  14051  2idlmex  14057  qusrhm  14084  znlidl  14190  zncrng2  14191  znval  14192  znle  14193  znbaslemnn  14195  znbas  14200  znzrh2  14202  znzrhval  14203  znzrhfo  14204  zndvds  14205  znfi  14211  znhash  14212  znidom  14213  znidomb  14214  psrval  14220  psrbasg  14227  psrelbas  14228  psrplusgg  14230  psraddcl  14232  toponsspwpwg  14258  topgele  14265  istps  14268  topontopn  14273  tgclb  14301  lmfval  14428  lmres  14484  ispsmet  14559  psmetge0  14567  ismet  14580  isxmet  14581  xmetge0  14601  isxms2  14688  comet  14735  bdxmet  14737  cnmetdval  14765  cnbl0  14770  cnblcld  14771  reopnap  14782  tgioo  14790  cncfcncntop  14829  cncfmpt2fcntop  14835  maxcncf  14851  mincncf  14852  hovergt0  14886  limcimolemlt  14900  cnplimcim  14903  cnplimclemr  14905  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  dvfvalap  14917  dvbss  14921  dvcnp2cntop  14935  dvcn  14936  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  dvmptfsum  14961  dveflem  14962  plyval  14968  plycolemc  14994  dvply2  15003  reeff1olem  15007  pilem3  15019  ef2kpi  15042  efper  15043  sinperlem  15044  efimpi  15055  ptolemy  15060  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  cosq14gt0  15068  tangtx  15074  sinkpi  15083  coskpi  15084  cosordlem  15085  rplogcl  15115  logge0  15116  logdivlti  15117  logbleb  15197  logblt  15198  binom4  15215  wilthlem1  15216  1sgmprm  15230  1sgm2ppw  15231  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsval2lem  15251  lgsval4a  15263  lgsneg  15265  lgsdilem  15268  lgsdirprm  15275  lgsdirnn0  15288  gausslemma2dlem0i  15298  gausslemma2dlem6  15308  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlemofi  15317  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem2  15323  lgsquad2  15324  m1lgs  15326  2lgs  15345  2lgsoddprmlem2  15347  2lgsoddprm  15354  2sqlem2  15356  pwf1oexmid  15644  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696