Theorem sylancl 417

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 415	1 |- ( ph -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  sylanblc  419  sylanblrc  420  equveli  1812  sseqtrid  3298  ssdifin0  3609  uneqdifeqim  3613  unimax  3969  opth  4377  djussxp  4925  iss  5109  relresfld  5317  eldmrexrn  5849  f1oresrab  5873  fmptco  5874  fsn  5880  fnressn  5901  foima2  5957  foeqcnvco  5996  isoini2  6025  relmptopab  6291  ofres  6317  ofco  6321  suppval1  6479  suppimacnvfn  6486  tposexg  6529  tfrlemisucaccv  6596  tfrlemibex  6600  tfri1dALT  6622  tfrcl  6635  rdgivallem  6652  frecabex  6669  frectfr  6671  frecrdg  6679  pmresg  6957  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpsnf1o  7018  en1  7086  2dom  7093  mapsnend  7099  enpr2d  7111  en2  7112  mapxpen  7148  mapunen  7151  phplem4  7156  exmidpw2en  7219  fiintim  7238  sbthlem2  7275  elfir  7307  2omap  7319  infglbti  7366  caseinl  7432  caseinr  7433  difinfsnlem  7440  difinfsn  7441  nninfisollemne  7472  exmidfodomrlemim  7554  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  2omotaplemap  7624  archnqq  7785  prarloclemlt  7861  prarloclemlo  7862  prarloclemcalc  7870  recexprlemm  7992  recexprlemex  8005  caucvgprlemm  8036  caucvgprprlemmu  8063  suplocexprlem2b  8082  suplocexprlemmu  8086  suplocexprlemlub  8092  1idsr  8136  recexgt0sr  8141  archsr  8150  caucvgsrlemoffval  8164  caucvgsrlemofff  8165  caucvgsrlemoffres  8168  caucvgsr  8170  ltpsrprg  8171  suplocsrlem  8176  pitonnlem2  8215  pitonn  8216  pitoregt0  8217  pitore  8218  recnnre  8219  axrnegex  8247  nntopi  8262  msqge0  8947  mulge0  8950  recexaplem2  8983  recexap  8984  recgt0  9183  recreclt  9233  nn1m1nn  9325  nn1suc  9326  nnle1eq1  9331  nn1gt1  9341  nnsub  9346  addltmul  9547  nn0le0eq0  9596  elnn0nn  9610  elnnz  9659  elznn0  9664  zlem1lt  9706  zltlem1  9707  elz2  9721  nn0n0n1ge2b  9730  nn0lt2  9732  nn0le2is012  9733  eluzaddi  9959  eluzsubi  9960  uzp1  9966  peano2uzr  9995  nn01to3  10027  qreccl  10052  irrmulap  10059  ltpnf  10193  xaddass2  10283  iccen  10420  fz01en  10470  fzpreddisj  10489  fzsuc2  10497  fseq1p1m1  10512  fseq1m1p1  10513  elfzp1b  10515  fzoss2  10592  fzval3  10633  fzosplitsnm1  10638  fzosplitprm1  10664  flhalf  10752  fldiv4lem1div2uz2  10756  modqmulnn  10794  modqmuladdnn0  10820  frec2uzrand  10857  frecuzrdg0  10865  frecuzrdg0t  10874  frecfzennn  10878  frecfzen2  10879  uzennn  10888  seqeq1  10902  seqp1g  10918  seqclg  10924  seq3m1  10925  monoord2  10938  ser3mono  10939  seqf1oglem1  10971  seqf1oglem2  10972  seqfeq4g  10983  ser0f  10986  exp3vallem  10992  expm1t  11019  expeq0  11022  expubnd  11048  binom3  11109  facndiv  11193  facavg  11200  bcn0  11209  bcnp1n  11213  bcm1k  11214  bcp1nk  11216  bcval5  11217  bcn2  11218  bcp1m1  11219  bcpasc  11220  bcn2m1  11224  hashsng  11253  hashun  11261  hashfz  11278  hashfzo  11279  hashmap  11284  hashfibclem  11298  hashf1lem1  11301  hashf1  11303  seq3coll  11310  hash2en  11311  iswrdiz  11327  snopiswrd  11330  ccat1st1st  11425  swrds1  11456  cats1un  11509  wrdind  11510  wrd2ind  11511  swrdccatin1  11513  swrdccat3blem  11527  shftfval  11602  2shfti  11612  resqrexlemf1  11790  abs00ap  11844  sqabs  11865  ltabs  11870  caubnd2  11900  max0addsup  12002  rexico  12004  mulcn2  12097  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  iserex  12124  climlec2  12126  iser3shft  12131  climcvg1nlem  12134  serf0  12137  sumrbdc  12165  fsumm1  12202  fsump1  12206  fsum00  12248  telfsumo  12252  fsumparts  12256  hashiun  12264  binomlem  12269  binom1dif  12273  bcxmas  12275  isumsplit  12277  isum1p  12278  arisum  12284  arisum2  12285  trireciplem  12286  explecnv  12291  geolim  12297  georeclim  12299  mertenslem2  12322  mertensabs  12323  prodf1f  12329  prodrbdclem2  12359  efcllemp  12444  ef0lem  12446  efgt0  12470  eftlub  12476  efsep  12477  effsumlt  12478  tanval3ap  12500  efi4p  12503  resin4p  12504  recos4p  12505  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sinltxirr  12547  sin01gt0  12548  cos01gt0  12549  absefib  12557  efieq1re  12558  eirraplem  12563  dvdsdc  12584  dvdscmulr  12606  fsumdvds  12628  dvdslelemd  12629  3dvds  12650  odd2np1lem  12658  odd2np1  12659  flodddiv4  12722  bitsfzo  12741  bitsmod  12742  gcdsupex  12753  gcdsupcl  12754  gcd1  12783  nninfctlemfo  12836  nn0seqcvgd  12838  algcvg  12845  algcvgblem  12846  eucalg  12856  prmind2  12917  qden1elz  13004  dfphi2  13021  phiprm  13024  phimullem  13026  prmdiv  13036  prmdiveq  13037  prm23lt5  13065  pcpre1  13094  pczpre  13099  pcdiv  13104  pc1  13107  pcqdiv  13109  pcexp  13111  pcxnn0cl  13112  pcxcl  13113  pcdvdstr  13129  pc2dvds  13132  sumhashdc  13149  fldivp1  13150  pcfaclem  13151  qexpz  13154  expnprm  13155  prmpwdvds  13157  pockthlem  13158  4sqlem5  13184  4sqlem6  13185  4sqlem11  13203  4sqlem13m  13205  4sqlem19  13211  prmlem1a  13244  ballotfilemofi  13271  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemodife  13292  ballotfilemscl  13299  ballotfilemsle  13300  oddennn  13335  xpct  13339  ennnfonelemj0  13344  ennnfonelemen  13364  ctinfomlemom  13370  omctfn  13386  restid  13657  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfnlemg  13688  xpscf  13721  gzsumvalx  13762  gzsumsplit1r  13768  gzsumcl  13857  mulgnngzsum  13983  mulgnndir  14007  mulgneg2  14012  cntrnsg  14170  gsumvalfi  14236  prdsex  14256  prdsval  14257  prdsbaslemss  14258  prdsbas  14260  prdsgrpd  14281  prdsinvgd  14282  dvdsrmuld  14487  zsssubrg  15006  znval  15055  znle  15056  znbaslemnn  15058  znf1o  15070  znleval  15072  psrval  15134  restuni2  15369  cnrest2r  15429  lmfss  15436  lmres  15440  lmtopcnp  15442  ispsmet  15515  isxmet2d  15540  ismet2  15546  blfvalps  15577  blex  15579  xblss2  15597  reopnap  15738  divcnap  15757  climcncf  15776  cncfmpt2fcntop  15791  hovera  15839  limcdifap  15854  cnplimcim  15859  cnlimcim  15863  cnlimc  15864  cnlimci  15865  dvbss  15877  dvcnp2cntop  15891  dvcn  15892  dvaddxxbr  15893  dvmulxxbr  15894  dvexp  15903  dveflem  15918  plyval  15924  elply2  15927  plyf  15929  plyss  15930  plyssc  15931  elplyr  15932  plyaddlem1  15939  plymullem1  15940  plyaddlem  15941  plymullem  15942  plyco  15951  plycj  15953  dvply1  15957  reeff1olem  15963  sinperlem  16001  sin2kpi  16004  cos2kpi  16005  sin2pim  16006  cos2pim  16007  cosq14gt0  16025  coseq0q4123  16027  tangtx  16031  abssinper  16039  sinkpi  16040  coskpi  16041  cosq34lt1  16043  logrpap0b  16070  logdivlti  16075  rpcxpsqrtth  16127  rpabscxpbnd  16137  binom4  16180  birthdaylem2  16187  birthdaylem3  16188  wilthlem1  16193  0sgm  16215  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  chtdif  16225  ppiqp1le  16228  ppidif  16230  ppiqeq0  16241  ppiqltx  16242  prmorcht  16243  1sgmprm  16249  1sgm2ppw  16250  ppiublem2  16253  ppiqub  16254  chtublem  16256  chtqub  16257  mersenne  16258  perfect1  16259  perfectlem1  16260  perfectlem2  16261  perfect  16262  bcp1ctr  16267  bclbnd  16268  bposlem1  16272  bposlem2  16273  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem9  16280  bpos  16281  lgslem1  16285  lgsval  16289  lgsfvalg  16290  lgsfcl2  16291  lgsfcl  16293  lgsval2lem  16295  lgsvalmod  16304  lgsneg  16309  lgsdilem  16312  lgsdir2lem3  16315  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgsabs1  16324  lgsprme0  16327  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem0d  16337  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem3  16348  gausslemma2dlem4  16349  gausslemma2dlem5a  16350  gausslemma2dlem5  16351  gausslemma2dlem6  16352  lgseisenlem2  16356  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem1  16366  lgsquad2lem2  16367  lgsquad2  16368  m1lgs  16370  2lgslem1  16376  2lgslem2  16377  2lgs  16389  2sqlem9  16409  2sqlem10  16410  ushgredgedg  16633  ushgredgedgloop  16635  uhgrspansubgrlem  16683  wlkvtxiedg  16752  wlkvtxiedgg  16753  wlk1walkdom  16766  upgr2wlkdc  16784  clwwlkccatlem  16807  umgrclwwlkge2  16809  clwwlknonmpo  16835  clwwlknonex2lem2  16845  clwwlknonex2  16846  konigsberglem1  16895  pwle2  17194  pw1nct  17199  nninfsellemdc  17219  nnnninfen  17230  nnnninfex  17231  nninfnfiinf  17232  sbthom  17237  repiecelem  17240  repiecele0  17241  trirec0  17260  apdifflemr  17263  reap0  17275  nconstwlpolem  17282