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  4106  unipw  4231  opeluu  4464  uniexb  4487  unon  4524  onintrab2im  4531  xpexg  4754  resiexg  4966  imaexg  4996  exse2  5016  soirri  5037  djudisj  5070  elxp5  5131  cnvexg  5180  cnviinm  5184  coexg  5187  funssres  5272  f1oabexg  5487  sefvex  5550  ssimaex  5592  mptfvex  5616  f1ompt  5682  fmptcof  5698  resfunexg  5752  mptexg  5756  funfvima3  5765  ovid  6007  ov  6010  ofres  6114  cofunexg  6127  opabex3d  6139  opabex3  6140  oprabexd  6145  1stcof  6181  2ndcof  6182  mpoexxg  6228  cnvf1o  6243  f2ndf  6244  algrflemg  6248  tposexg  6276  tfrlemisucaccv  6343  tfrlemibxssdm  6345  tfrlemibfn  6346  tfrlemi14d  6351  tfr1onlemsucaccv  6359  tfr1onlembxssdm  6361  tfr1onlembfn  6362  tfr1onlemres  6367  tfrcllemsucaccv  6372  tfrcllembxssdm  6374  tfrcllembfn  6375  tfrcllemres  6380  rdgtfr  6392  rdgruledefgg  6393  rdgon  6404  frecabex  6416  freccllem  6420  frecfcllem  6422  omcl  6479  oeicl  6480  erth  6596  th3qlem1  6654  mapex  6671  pmvalg  6676  mapsnconst  6711  ixpexgg  6739  fundmen  6823  cnvct  6826  snfig  6831  unen  6833  xpdom2  6848  mapxpen  6865  phplem2  6870  findcard2  6906  findcard2s  6907  infnfi  6912  relcnvfi  6957  sbthlemi8  6980  sbthlemi10  6982  fival  6986  fiss  6993  inl11  7081  casef  7104  caseinj  7105  caseinl  7107  caseinr  7108  djudom  7109  difinfsn  7116  djuinj  7122  0ct  7123  ctmlemr  7124  ctssdccl  7127  enomnilem  7153  enmkvlem  7176  enwomnilem  7184  djuassen  7233  xpdjuen  7234  djudoml  7235  djudomr  7236  cc2lem  7282  ltnnnq  7439  nnnq0lem1  7462  addnqprlemfl  7575  addnqprlemfu  7576  mulnqprlemfl  7591  mulnqprlemfu  7592  suplocexprlem2b  7730  prsrlem1  7758  gt0srpr  7764  caucvgsrlemcl  7805  caucvgsrlemfv  7807  caucvgsrlembound  7810  mulcnsr  7851  mulcnsrec  7859  addvalex  7860  pitoregt0  7865  axmulass  7889  axdistr  7890  recriota  7906  mulrid  7971  axmulgt0  8046  cnegexlem2  8150  cnegex  8152  gt0ne0d  8486  recexre  8552  msqge0  8590  mulge0  8593  aptap  8624  recgt0  8824  recreclt  8874  cju  8935  nnge1  8959  nnnlt1  8962  nn0nlt0  9219  elz2  9341  nnm1ge0  9356  recnz  9363  zneo  9371  uz3m2nn  9590  eluz2b2  9620  nn01to3  9634  mnflt  9800  xnn0dcle  9819  xltadd1  9893  lincmb01cmp  10020  iccf1o  10021  fz1n  10061  fseq1p1m1  10111  fznn0  10130  fzctr  10150  4fvwrd4  10157  elfzonlteqm1  10227  divfl0  10313  modqelico  10351  zmodfz  10363  modqid  10366  modqmuladdim  10384  m1modge3gt1  10388  addmodid  10389  frec2uzf1od  10423  frecfzennn  10443  frecfzen2  10444  fzfig  10447  ser0  10531  ser3le  10535  expgt1  10575  expubnd  10594  iexpcyc  10642  binom2sub  10651  binom3  10655  zesq  10656  bernneq  10658  bernneq2  10659  expnbnd  10661  expnlbnd2  10663  facdiv  10735  faclbnd2  10739  faclbnd3  10740  bcval4  10749  hashinfom  10775  hashennn  10777  fihashf1rn  10785  isfinite4im  10789  hashfz  10818  crre  10883  crim  10884  remim  10886  mulreap  10890  cjreb  10892  recj  10893  reneg  10894  readd  10895  remullem  10897  imcj  10901  imneg  10902  imadd  10903  cjadd  10910  cjneg  10916  imval2  10920  cjreim  10929  cnrecnv  10936  uzin2  11013  absval  11027  rennim  11028  resqrexlemcalc3  11042  resqrexlemnm  11044  resqrexlemcvg  11045  resqrexlemgt0  11046  resqrexlemga  11049  absreimsq  11093  absreim  11094  amgm2  11144  climconst2  11316  climshft  11329  climshft2  11331  reccn2ap  11338  climge0  11350  sumsnf  11434  sumnul  11449  isumcl  11450  fsum2dlemstep  11459  fisumcom2  11463  fsumabs  11490  fsumiun  11502  binom  11509  bcxmas  11514  arisum  11523  expcnvap0  11527  explecnv  11530  geosergap  11531  geolim  11536  geolim2  11537  geo2sum  11539  geo2lim  11541  cvgratnnlemrate  11555  cvgratz  11557  mertenslemi1  11560  prodf1  11567  prodeq2w  11581  fprodntrivap  11609  prodsnf  11617  fprod2dlemstep  11647  fprodcom2fi  11651  efcllemp  11683  ege2le3  11696  eftlub  11715  efgt1  11722  tanval2ap  11738  tanval3ap  11739  resinval  11740  recosval  11741  efi4p  11742  resin4p  11743  recos4p  11744  resincl  11745  recoscl  11746  efmival  11758  efeul  11759  sinadd  11761  cosadd  11762  tanaddap  11764  sinmul  11769  cos2tsin  11776  ef01bndlem  11781  sin01bnd  11782  cos01bnd  11783  sin01gt0  11786  cos01gt0  11787  absef  11794  absefib  11795  efieq1re  11796  demoivreALT  11798  eirraplem  11801  odd2np1  11895  oddm1even  11897  oddp1even  11898  oexpneg  11899  opoe  11917  omoe  11918  nn0o1gt2  11927  nn0o  11929  algcvg  12065  algcvgblem  12066  1nprm  12131  1idssfct  12132  oddprmge3  12152  divgcdodd  12160  pw2dvdslemn  12182  pw2dvds  12183  oddpwdclemodd  12189  oddpwdc  12191  phicl2  12231  phibndlem  12233  phibnd  12234  hashdvds  12238  crth  12241  phimullem  12242  eulerthlemfi  12245  eulerthlemrprm  12246  eulerthlema  12247  hashgcdeq  12256  phisum  12257  oddprm  12276  prm23ge5  12281  pythagtriplem1  12282  pythagtriplem4  12285  pythagtriplem12  12292  pythagtriplem14  12294  pczpre  12314  pcadd  12356  pcmpt  12358  pockthlem  12371  pockthi  12373  infpnlem2  12375  gzreim  12394  evenennn  12411  ennnfonelemjn  12420  ennnfonelemkh  12430  ennnfonelemhf1o  12431  ennnfonelemex  12432  ennnfonelemhom  12433  ennnfonelemnn0  12440  exmidunben  12444  ctinfomlemom  12445  ssnnctlemct  12464  nninfdc  12471  slotex  12506  setscom  12519  setsslid  12530  basmex  12538  basmexd  12539  ressbas2d  12545  ressbasid  12547  strressid  12548  ressval3d  12549  2strbas1g  12599  2strop1g  12600  rngbaseg  12612  rngplusgg  12613  rngmulrg  12614  srngbased  12623  srngplusgd  12624  srngmulrd  12625  srnginvld  12626  lmodbased  12641  lmodplusgd  12642  lmodscad  12643  lmodvscad  12644  ipsbased  12653  ipsaddgd  12654  ipsmulrd  12655  ipsscad  12656  ipsvscad  12657  ipsipd  12658  topgrpbasd  12673  topgrpplusgd  12674  topgrptsetd  12675  tgvalex  12733  prdsex  12739  imasex  12747  imasival  12748  imasbas  12749  imasplusg  12750  imasmulr  12751  imasaddfn  12759  imasaddval  12760  imasaddf  12761  imasmulfn  12762  imasmulval  12763  imasmulf  12764  qusval  12765  qusex  12767  qusaddvallemg  12774  qusaddflemg  12775  qusaddval  12776  qusaddf  12777  qusmulval  12778  qusmulf  12779  xpsfval  12789  xpsval  12793  plusffvalg  12803  grpidvalg  12814  issubmnd  12868  ress0g  12869  ismhm  12878  mhmex  12879  issubm  12889  0mhm  12903  grppropstrg  12929  grpinvfvalg  12951  grpinvval  12952  grpinvfng  12953  grpsubfvalg  12954  grpsubval  12955  grpressid  12970  grplactfval  13010  qusgrp2  13020  mulgfvalg  13028  mulgex  13030  issubg  13077  subgex  13080  subgmulg  13092  issubg2m  13093  releqgg  13124  eqgex  13125  eqgfval  13126  eqgen  13131  isghm  13142  ablressid  13232  mgptopng  13243  rngressid  13268  qusrng  13272  dfur2g  13276  ringidss  13343  ring1  13371  ringressid  13373  qusring2  13376  reldvdsrsrg  13402  dvdsrvald  13403  dvdsrex  13408  unitgrp  13426  unitabl  13427  invrfvald  13432  unitlinv  13436  unitrinv  13437  dvrfvald  13443  rdivmuldivd  13454  invrpropdg  13459  rhmunitinv  13488  issubrng  13506  issubrg  13528  subrgugrp  13547  subrgpropd  13555  aprval  13558  islmod  13567  scaffvalg  13582  lssex  13630  lssmex  13631  lsssetm  13632  islssmg  13634  islss3  13655  lspfval  13664  lspval  13666  lspcl  13667  lspex  13671  sralemg  13714  srascag  13718  sravscag  13719  sraipg  13720  sraex  13722  rlmsubg  13734  rlmvnegg  13741  ixpsnbasval  13742  lidlvalg  13747  rspvalg  13748  lidlex  13749  rspex  13750  lidlmex  13751  lidlss  13752  lidlrsppropdg  13771  2idlmex  13778  znlidl  13879  toponsspwpwg  13905  topgele  13912  istps  13915  topontopn  13920  tgclb  13948  lmfval  14075  lmres  14131  ispsmet  14206  psmetge0  14214  ismet  14227  isxmet  14228  xmetge0  14248  isxms2  14335  comet  14382  bdxmet  14384  cnmetdval  14412  cnbl0  14417  cnblcld  14418  reopnap  14421  tgioo  14429  cncfcncntop  14463  cncfmpt2fcntop  14468  limcimolemlt  14516  cnplimcim  14519  cnplimclemr  14521  limccnpcntop  14527  limccnp2lem  14528  limccnp2cntop  14529  dvfvalap  14533  dvbss  14537  dvcnp2cntop  14546  dvcn  14547  dvaddxxbr  14548  dvmulxxbr  14549  dvcoapbr  14554  dvcjbr  14555  dvrecap  14560  dveflem  14570  reeff1olem  14575  pilem3  14587  ef2kpi  14610  efper  14611  sinperlem  14612  efimpi  14623  ptolemy  14628  sincosq2sgn  14631  sincosq3sgn  14632  sincosq4sgn  14633  sinq12gt0  14634  cosq14gt0  14636  tangtx  14642  sinkpi  14651  coskpi  14652  cosordlem  14653  rplogcl  14683  logge0  14684  logdivlti  14685  logbleb  14762  logblt  14763  binom4  14780  lgsval2lem  14794  lgsval4a  14806  lgsneg  14808  lgsdilem  14811  lgsdirprm  14818  lgsdirnn0  14831  lgseisenlem1  14833  lgseisenlem2  14834  m1lgs  14835  2lgsoddprmlem2  14837  2sqlem2  14845  pwf1oexmid  15133  isomninnlem  15162  iswomninnlem  15181  ismkvnnlem  15184