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  4093  unipw  4218  opeluu  4451  uniexb  4474  unon  4511  onintrab2im  4518  xpexg  4741  resiexg  4953  imaexg  4983  exse2  5003  soirri  5024  djudisj  5057  elxp5  5118  cnvexg  5167  cnviinm  5171  coexg  5174  funssres  5259  f1oabexg  5474  sefvex  5537  ssimaex  5578  mptfvex  5602  f1ompt  5668  fmptcof  5684  resfunexg  5738  mptexg  5742  funfvima3  5751  ovid  5991  ov  5994  ofres  6097  cofunexg  6110  opabex3d  6122  opabex3  6123  oprabexd  6128  1stcof  6164  2ndcof  6165  mpoexxg  6211  cnvf1o  6226  f2ndf  6227  algrflemg  6231  tposexg  6259  tfrlemisucaccv  6326  tfrlemibxssdm  6328  tfrlemibfn  6329  tfrlemi14d  6334  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemres  6350  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemres  6363  rdgtfr  6375  rdgruledefgg  6376  rdgon  6387  frecabex  6399  freccllem  6403  frecfcllem  6405  omcl  6462  oeicl  6463  erth  6579  th3qlem1  6637  mapex  6654  pmvalg  6659  mapsnconst  6694  ixpexgg  6722  fundmen  6806  cnvct  6809  snfig  6814  unen  6816  xpdom2  6831  mapxpen  6848  phplem2  6853  findcard2  6889  findcard2s  6890  infnfi  6895  relcnvfi  6940  sbthlemi8  6963  sbthlemi10  6965  fival  6969  fiss  6976  inl11  7064  casef  7087  caseinj  7088  caseinl  7090  caseinr  7091  djudom  7092  difinfsn  7099  djuinj  7105  0ct  7106  ctmlemr  7107  ctssdccl  7110  enomnilem  7136  enmkvlem  7159  enwomnilem  7167  djuassen  7216  xpdjuen  7217  djudoml  7218  djudomr  7219  cc2lem  7265  ltnnnq  7422  nnnq0lem1  7445  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemfl  7574  mulnqprlemfu  7575  suplocexprlem2b  7713  prsrlem1  7741  gt0srpr  7747  caucvgsrlemcl  7788  caucvgsrlemfv  7790  caucvgsrlembound  7793  mulcnsr  7834  mulcnsrec  7842  addvalex  7843  pitoregt0  7848  axmulass  7872  axdistr  7873  recriota  7889  mulrid  7954  axmulgt0  8029  cnegexlem2  8133  cnegex  8135  gt0ne0d  8469  recexre  8535  msqge0  8573  mulge0  8576  aptap  8607  recgt0  8807  recreclt  8857  cju  8918  nnge1  8942  nnnlt1  8945  nn0nlt0  9202  elz2  9324  nnm1ge0  9339  recnz  9346  zneo  9354  uz3m2nn  9573  eluz2b2  9603  nn01to3  9617  mnflt  9783  xnn0dcle  9802  xltadd1  9876  lincmb01cmp  10003  iccf1o  10004  fz1n  10044  fseq1p1m1  10094  fznn0  10113  fzctr  10133  4fvwrd4  10140  elfzonlteqm1  10210  divfl0  10296  modqelico  10334  zmodfz  10346  modqid  10349  modqmuladdim  10367  m1modge3gt1  10371  addmodid  10372  frec2uzf1od  10406  frecfzennn  10426  frecfzen2  10427  fzfig  10430  ser0  10514  ser3le  10518  expgt1  10558  expubnd  10577  iexpcyc  10625  binom2sub  10634  binom3  10638  zesq  10639  bernneq  10641  bernneq2  10642  expnbnd  10644  expnlbnd2  10646  facdiv  10718  faclbnd2  10722  faclbnd3  10723  bcval4  10732  hashinfom  10758  hashennn  10760  fihashf1rn  10768  isfinite4im  10772  hashfz  10801  crre  10866  crim  10867  remim  10869  mulreap  10873  cjreb  10875  recj  10876  reneg  10877  readd  10878  remullem  10880  imcj  10884  imneg  10885  imadd  10886  cjadd  10893  cjneg  10899  imval2  10903  cjreim  10912  cnrecnv  10919  uzin2  10996  absval  11010  rennim  11011  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemcvg  11028  resqrexlemgt0  11029  resqrexlemga  11032  absreimsq  11076  absreim  11077  amgm2  11127  climconst2  11299  climshft  11312  climshft2  11314  reccn2ap  11321  climge0  11333  sumsnf  11417  sumnul  11432  isumcl  11433  fsum2dlemstep  11442  fisumcom2  11446  fsumabs  11473  fsumiun  11485  binom  11492  bcxmas  11497  arisum  11506  expcnvap0  11510  explecnv  11513  geosergap  11514  geolim  11519  geolim2  11520  geo2sum  11522  geo2lim  11524  cvgratnnlemrate  11538  cvgratz  11540  mertenslemi1  11543  prodf1  11550  prodeq2w  11564  fprodntrivap  11592  prodsnf  11600  fprod2dlemstep  11630  fprodcom2fi  11634  efcllemp  11666  ege2le3  11679  eftlub  11698  efgt1  11705  tanval2ap  11721  tanval3ap  11722  resinval  11723  recosval  11724  efi4p  11725  resin4p  11726  recos4p  11727  resincl  11728  recoscl  11729  efmival  11741  efeul  11742  sinadd  11744  cosadd  11745  tanaddap  11747  sinmul  11752  cos2tsin  11759  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  sin01gt0  11769  cos01gt0  11770  absef  11777  absefib  11778  efieq1re  11779  demoivreALT  11781  eirraplem  11784  odd2np1  11878  oddm1even  11880  oddp1even  11881  oexpneg  11882  opoe  11900  omoe  11901  nn0o1gt2  11910  nn0o  11912  algcvg  12048  algcvgblem  12049  1nprm  12114  1idssfct  12115  oddprmge3  12135  divgcdodd  12143  pw2dvdslemn  12165  pw2dvds  12166  oddpwdclemodd  12172  oddpwdc  12174  phicl2  12214  phibndlem  12216  phibnd  12217  hashdvds  12221  crth  12224  phimullem  12225  eulerthlemfi  12228  eulerthlemrprm  12229  eulerthlema  12230  hashgcdeq  12239  phisum  12240  oddprm  12259  prm23ge5  12264  pythagtriplem1  12265  pythagtriplem4  12268  pythagtriplem12  12275  pythagtriplem14  12277  pczpre  12297  pcadd  12339  pcmpt  12341  pockthlem  12354  pockthi  12356  infpnlem2  12358  gzreim  12377  evenennn  12394  ennnfonelemjn  12403  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemnn0  12423  exmidunben  12427  ctinfomlemom  12428  ssnnctlemct  12447  nninfdc  12454  slotex  12489  setscom  12502  setsslid  12513  basmex  12521  basmexd  12522  ressbas2d  12528  strressid  12530  ressval3d  12531  2strbas1g  12581  2strop1g  12582  rngbaseg  12594  rngplusgg  12595  rngmulrg  12596  srngbased  12605  srngplusgd  12606  srngmulrd  12607  srnginvld  12608  lmodbased  12623  lmodplusgd  12624  lmodscad  12625  lmodvscad  12626  ipsbased  12635  ipsaddgd  12636  ipsmulrd  12637  ipsscad  12638  ipsvscad  12639  ipsipd  12640  topgrpbasd  12652  topgrpplusgd  12653  topgrptsetd  12654  tgvalex  12712  prdsex  12718  imasex  12726  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfn  12738  imasaddval  12739  imasaddf  12740  imasmulfn  12741  imasmulval  12742  imasmulf  12743  qusval  12744  qusaddvallemg  12752  qusaddflemg  12753  qusaddval  12754  qusaddf  12755  qusmulval  12756  qusmulf  12757  xpsfval  12767  xpsval  12771  plusffvalg  12781  grpidvalg  12792  issubmnd  12843  ress0g  12844  ismhm  12853  issubm  12863  0mhm  12873  grppropstrg  12895  grpinvfvalg  12915  grpinvval  12916  grpinvfng  12917  grpsubfvalg  12918  grpsubval  12919  grpressid  12931  grplactfval  12971  mulgfvalg  12985  issubg  13033  subgex  13036  subgmulg  13048  issubg2m  13049  releqgg  13080  eqgfval  13081  eqgen  13086  mgptopng  13139  dfur2g  13145  ringidss  13212  ring1  13236  ringressid  13238  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrex  13267  unitgrp  13285  unitabl  13286  invrfvald  13291  unitlinv  13295  unitrinv  13296  dvrfvald  13302  rdivmuldivd  13313  invrpropdg  13318  issubrg  13342  subrgugrp  13361  subrgpropd  13369  aprval  13372  islmod  13381  scaffvalg  13396  toponsspwpwg  13525  topgele  13532  istps  13535  topontopn  13540  tgclb  13568  lmfval  13695  lmres  13751  ispsmet  13826  psmetge0  13834  ismet  13847  isxmet  13848  xmetge0  13868  isxms2  13955  comet  14002  bdxmet  14004  cnmetdval  14032  cnbl0  14037  cnblcld  14038  reopnap  14041  tgioo  14049  cncfcncntop  14083  cncfmpt2fcntop  14088  limcimolemlt  14136  cnplimcim  14139  cnplimclemr  14141  limccnpcntop  14147  limccnp2lem  14148  limccnp2cntop  14149  dvfvalap  14153  dvbss  14157  dvcnp2cntop  14166  dvcn  14167  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvrecap  14180  dveflem  14190  reeff1olem  14195  pilem3  14207  ef2kpi  14230  efper  14231  sinperlem  14232  efimpi  14243  ptolemy  14248  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  cosq14gt0  14256  tangtx  14262  sinkpi  14271  coskpi  14272  cosordlem  14273  rplogcl  14303  logge0  14304  logdivlti  14305  logbleb  14382  logblt  14383  binom4  14400  lgsval2lem  14414  lgsval4a  14426  lgsneg  14428  lgsdilem  14431  lgsdirprm  14438  lgsdirnn0  14451  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2lgsoddprmlem2  14457  2sqlem2  14465  pwf1oexmid  14752  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803