Theorem sylancl 413

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancl.1	|- ( ph -> ps )
sylancl.2	|- ch
sylancl.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylancl	|- ( ph -> th )

Proof of Theorem sylancl

Step	Hyp	Ref	Expression
1		sylancl.1	. 2 |- ( ph -> ps )
2		sylancl.2	. . 3 |- ch
3	2	a1i 9	. 2 |- ( ph -> ch )
4		sylancl.3	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 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:  sylanblc  415  sylanblrc  416  equveli  1808  sseqtrid  3292  ssdifin0  3595  uneqdifeqim  3599  unimax  3953  opth  4358  djussxp  4905  iss  5089  relresfld  5297  eldmrexrn  5823  f1oresrab  5847  fmptco  5848  fsn  5854  fnressn  5875  foima2  5930  foeqcnvco  5969  isoini2  5998  relmptopab  6264  ofres  6290  ofco  6294  suppval1  6452  suppimacnvfn  6459  tposexg  6502  tfrlemisucaccv  6569  tfrlemibex  6573  tfri1dALT  6595  tfrcl  6608  rdgivallem  6625  frecabex  6642  frectfr  6644  frecrdg  6652  pmresg  6923  mapsnd  6936  mapsn  6938  mapsncnv  6943  ixpsnf1o  6984  en1  7052  2dom  7059  mapsnend  7065  enpr2d  7077  en2  7078  mapxpen  7114  mapunen  7117  phplem4  7122  exmidpw2en  7185  fiintim  7204  sbthlem2  7241  elfir  7273  2omap  7282  infglbti  7329  caseinl  7395  caseinr  7396  difinfsnlem  7403  difinfsn  7404  nninfisollemne  7435  exmidfodomrlemim  7517  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  2omotaplemap  7587  archnqq  7748  prarloclemlt  7824  prarloclemlo  7825  prarloclemcalc  7833  recexprlemm  7955  recexprlemex  7968  caucvgprlemm  7999  caucvgprprlemmu  8026  suplocexprlem2b  8045  suplocexprlemmu  8049  suplocexprlemlub  8055  1idsr  8099  recexgt0sr  8104  archsr  8113  caucvgsrlemoffval  8127  caucvgsrlemofff  8128  caucvgsrlemoffres  8131  caucvgsr  8133  ltpsrprg  8134  suplocsrlem  8139  pitonnlem2  8178  pitonn  8179  pitoregt0  8180  pitore  8181  recnnre  8182  axrnegex  8210  nntopi  8225  msqge0  8907  mulge0  8910  recexaplem2  8943  recexap  8944  recgt0  9141  recreclt  9191  nn1m1nn  9272  nn1suc  9273  nnle1eq1  9278  nn1gt1  9288  nnsub  9293  addltmul  9492  nn0le0eq0  9541  elnn0nn  9555  elnnz  9604  elznn0  9609  zlem1lt  9651  zltlem1  9652  elz2  9666  nn0n0n1ge2b  9675  nn0lt2  9677  nn0le2is012  9678  eluzaddi  9899  eluzsubi  9900  uzp1  9906  peano2uzr  9935  nn01to3  9967  qreccl  9992  irrmulap  9998  ltpnf  10132  xaddass2  10222  iccen  10359  fz01en  10408  fzpreddisj  10427  fzsuc2  10435  fseq1p1m1  10450  fseq1m1p1  10451  elfzp1b  10453  fzoss2  10530  fzval3  10571  fzosplitsnm1  10576  fzosplitprm1  10602  flhalf  10686  fldiv4lem1div2uz2  10690  modqmulnn  10728  modqmuladdnn0  10754  frec2uzrand  10791  frecuzrdg0  10799  frecuzrdg0t  10808  frecfzennn  10812  frecfzen2  10813  uzennn  10822  seqeq1  10836  seqp1g  10852  seqclg  10858  seq3m1  10859  monoord2  10872  ser3mono  10873  seqf1oglem1  10905  seqf1oglem2  10906  seqfeq4g  10917  ser0f  10920  exp3vallem  10926  expm1t  10953  expeq0  10956  expubnd  10982  binom3  11043  facndiv  11126  facavg  11133  bcn0  11142  bcnp1n  11146  bcm1k  11147  bcp1nk  11149  bcval5  11150  bcn2  11151  bcp1m1  11152  bcpasc  11153  bcn2m1  11157  hashsng  11186  hashun  11194  hashfz  11211  hashfzo  11212  hashmap  11217  hashfibclem  11231  seq3coll  11239  hash2en  11240  iswrdiz  11256  snopiswrd  11259  ccat1st1st  11354  swrds1  11385  cats1un  11438  wrdind  11439  wrd2ind  11440  swrdccatin1  11442  swrdccat3blem  11456  shftfval  11531  2shfti  11541  resqrexlemf1  11718  abs00ap  11772  sqabs  11792  ltabs  11797  caubnd2  11827  max0addsup  11929  rexico  11931  mulcn2  12022  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  iserex  12049  climlec2  12051  iser3shft  12056  climcvg1nlem  12059  serf0  12062  sumrbdc  12090  fsumm1  12127  fsump1  12131  fsum00  12173  telfsumo  12177  fsumparts  12181  hashiun  12189  binomlem  12194  binom1dif  12198  bcxmas  12200  isumsplit  12202  isum1p  12203  arisum  12209  arisum2  12210  trireciplem  12211  explecnv  12216  geolim  12222  georeclim  12224  mertenslem2  12247  mertensabs  12248  prodf1f  12254  prodrbdclem2  12284  efcllemp  12369  ef0lem  12371  efgt0  12395  eftlub  12401  efsep  12402  effsumlt  12403  tanval3ap  12425  efi4p  12428  resin4p  12429  recos4p  12430  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sinltxirr  12472  sin01gt0  12473  cos01gt0  12474  absefib  12482  efieq1re  12483  eirraplem  12488  dvdsdc  12509  dvdscmulr  12531  fsumdvds  12553  dvdslelemd  12554  3dvds  12575  odd2np1lem  12583  odd2np1  12584  flodddiv4  12647  bitsfzo  12666  bitsmod  12667  gcdsupex  12678  gcdsupcl  12679  gcd1  12708  nninfctlemfo  12761  nn0seqcvgd  12763  algcvg  12770  algcvgblem  12771  eucalg  12781  prmind2  12842  qden1elz  12927  dfphi2  12942  phiprm  12945  phimullem  12947  prmdiv  12957  prmdiveq  12958  prm23lt5  12986  pcpre1  13015  pczpre  13020  pcdiv  13025  pc1  13028  pcqdiv  13030  pcexp  13032  pcxnn0cl  13033  pcxcl  13034  pcdvdstr  13050  pc2dvds  13053  sumhashdc  13070  fldivp1  13071  pcfaclem  13072  qexpz  13075  expnprm  13076  prmpwdvds  13078  pockthlem  13079  4sqlem5  13105  4sqlem6  13106  4sqlem11  13124  4sqlem13m  13126  4sqlem19  13132  ballotfilemofi  13163  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilemscl  13191  ballotfilemsle  13192  oddennn  13227  xpct  13231  ennnfonelemj0  13236  ennnfonelemen  13256  ctinfomlemom  13262  omctfn  13278  restid  13547  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfnlemg  13578  xpscf  13611  igsumvalx  13652  gsumsplit1r  13661  gsumprval  13662  gsumfzz  13750  gsumfzcl  13754  mulgnngsum  13880  mulgnndir  13904  mulgneg2  13909  gfsumval  14102  prdsex  14114  prdsval  14115  prdsbaslemss  14116  prdsbas  14118  prdsgrpd  14139  prdsinvgd  14140  dvdsrmuld  14341  zsssubrg  14859  znval  14910  znle  14911  znbaslemnn  14913  znf1o  14925  znleval  14927  psrval  14940  restuni2  15168  cnrest2r  15228  lmfss  15235  lmres  15239  lmtopcnp  15241  ispsmet  15314  isxmet2d  15339  ismet2  15345  blfvalps  15376  blex  15378  xblss2  15396  reopnap  15537  divcnap  15556  climcncf  15575  cncfmpt2fcntop  15590  hovera  15638  limcdifap  15653  cnplimcim  15658  cnlimcim  15662  cnlimc  15663  cnlimci  15664  dvbss  15676  dvcnp2cntop  15690  dvcn  15691  dvaddxxbr  15692  dvmulxxbr  15693  dvexp  15702  dveflem  15717  plyval  15723  elply2  15726  plyf  15728  plyss  15729  plyssc  15730  elplyr  15731  plyaddlem1  15738  plymullem1  15739  plyaddlem  15740  plymullem  15741  plyco  15750  plycj  15752  dvply1  15756  reeff1olem  15762  sinperlem  15799  sin2kpi  15802  cos2kpi  15803  sin2pim  15804  cos2pim  15805  cosq14gt0  15823  coseq0q4123  15825  tangtx  15829  abssinper  15837  sinkpi  15838  coskpi  15839  cosq34lt1  15841  logrpap0b  15867  logdivlti  15872  rpcxpsqrtth  15921  rpabscxpbnd  15931  binom4  15970  wilthlem1  15974  0sgm  15979  1sgmprm  15988  1sgm2ppw  15989  mersenne  15991  perfect1  15992  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgslem1  15999  lgsval  16003  lgsfvalg  16004  lgsfcl2  16005  lgsfcl  16007  lgsval2lem  16009  lgsvalmod  16018  lgsneg  16023  lgsdilem  16026  lgsdir2lem3  16029  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsabs1  16038  lgsprme0  16041  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem0d  16051  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem3  16062  gausslemma2dlem4  16063  gausslemma2dlem5a  16064  gausslemma2dlem5  16065  gausslemma2dlem6  16066  lgseisenlem2  16070  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  lgsquad2lem2  16081  lgsquad2  16082  m1lgs  16084  2lgslem1  16090  2lgslem2  16091  2lgs  16103  2sqlem9  16123  2sqlem10  16124  ushgredgedg  16347  ushgredgedgloop  16349  uhgrspansubgrlem  16397  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlk1walkdom  16480  upgr2wlkdc  16498  clwwlkccatlem  16521  umgrclwwlkge2  16523  clwwlknonmpo  16549  clwwlknonex2lem2  16559  clwwlknonex2  16560  konigsberglem1  16609  pwle2  16898  pw1nct  16903  nninfsellemdc  16914  nnnninfen  16925  nnnninfex  16926  nninfnfiinf  16927  sbthom  16932  repiecelem  16935  repiecele0  16936  trirec0  16954  apdifflemr  16957  reap0  16969  trimul0or  16971  nconstwlpolem  16977