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  1807  sseqtrid  3277  ssdifin0  3576  uneqdifeqim  3580  unimax  3927  opth  4329  djussxp  4875  iss  5059  relresfld  5266  eldmrexrn  5788  f1oresrab  5812  fmptco  5813  fsn  5819  fnressn  5840  foima2  5892  foeqcnvco  5931  isoini2  5960  relmptopab  6224  ofres  6250  ofco  6254  tposexg  6424  tfrlemisucaccv  6491  tfrlemibex  6495  tfri1dALT  6517  tfrcl  6530  rdgivallem  6547  frecabex  6564  frectfr  6566  frecrdg  6574  pmresg  6845  mapsn  6859  mapsncnv  6864  ixpsnf1o  6905  en1  6973  2dom  6980  enpr2d  6997  en2  6998  mapxpen  7034  phplem4  7041  exmidpw2en  7104  fiintim  7123  sbthlem2  7157  elfir  7172  infglbti  7224  caseinl  7290  caseinr  7291  difinfsnlem  7298  difinfsn  7299  nninfisollemne  7330  exmidfodomrlemim  7412  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  2omotaplemap  7476  archnqq  7637  prarloclemlt  7713  prarloclemlo  7714  prarloclemcalc  7722  recexprlemm  7844  recexprlemex  7857  caucvgprlemm  7888  caucvgprprlemmu  7915  suplocexprlem2b  7934  suplocexprlemmu  7938  suplocexprlemlub  7944  1idsr  7988  recexgt0sr  7993  archsr  8002  caucvgsrlemoffval  8016  caucvgsrlemofff  8017  caucvgsrlemoffres  8020  caucvgsr  8022  ltpsrprg  8023  suplocsrlem  8028  pitonnlem2  8067  pitonn  8068  pitoregt0  8069  pitore  8070  recnnre  8071  axrnegex  8099  nntopi  8114  msqge0  8796  mulge0  8799  recexaplem2  8832  recexap  8833  recgt0  9030  recreclt  9080  nn1m1nn  9161  nn1suc  9162  nnle1eq1  9167  nn1gt1  9177  nnsub  9182  addltmul  9381  nn0le0eq0  9430  elnn0nn  9444  elnnz  9489  elznn0  9494  zlem1lt  9536  zltlem1  9537  elz2  9551  nn0n0n1ge2b  9559  nn0lt2  9561  nn0le2is012  9562  eluzaddi  9783  eluzsubi  9784  uzp1  9790  peano2uzr  9819  nn01to3  9851  qreccl  9876  irrmulap  9882  ltpnf  10015  xaddass2  10105  iccen  10241  fz01en  10288  fzpreddisj  10306  fzsuc2  10314  fseq1p1m1  10329  fseq1m1p1  10330  elfzp1b  10332  fzoss2  10409  fzval3  10450  fzosplitsnm1  10455  fzosplitprm1  10481  flhalf  10563  fldiv4lem1div2uz2  10567  modqmulnn  10605  modqmuladdnn0  10631  frec2uzrand  10668  frecuzrdg0  10676  frecuzrdg0t  10685  frecfzennn  10689  frecfzen2  10690  uzennn  10699  seqeq1  10713  seqp1g  10729  seqclg  10735  seq3m1  10736  monoord2  10749  ser3mono  10750  seqf1oglem1  10782  seqf1oglem2  10783  seqfeq4g  10794  ser0f  10797  exp3vallem  10803  expm1t  10830  expeq0  10833  expubnd  10859  binom3  10920  facndiv  11002  facavg  11009  bcn0  11018  bcnp1n  11022  bcm1k  11023  bcp1nk  11025  bcval5  11026  bcn2  11027  bcp1m1  11028  bcpasc  11029  bcn2m1  11032  hashsng  11061  hashun  11069  hashfz  11086  hashfzo  11087  seq3coll  11107  hash2en  11108  iswrdiz  11124  snopiswrd  11127  ccat1st1st  11222  swrds1  11253  cats1un  11306  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccat3blem  11324  shftfval  11399  2shfti  11409  resqrexlemf1  11586  abs00ap  11640  sqabs  11660  ltabs  11665  caubnd2  11695  max0addsup  11797  rexico  11799  mulcn2  11890  climaddc1  11907  climmulc2  11909  climsubc1  11910  climsubc2  11911  iserex  11917  climlec2  11919  iser3shft  11924  climcvg1nlem  11927  serf0  11930  sumrbdc  11958  fsumm1  11995  fsump1  11999  fsum00  12041  telfsumo  12045  fsumparts  12049  hashiun  12057  binomlem  12062  binom1dif  12066  bcxmas  12068  isumsplit  12070  isum1p  12071  arisum  12077  arisum2  12078  trireciplem  12079  explecnv  12084  geolim  12090  georeclim  12092  mertenslem2  12115  mertensabs  12116  prodf1f  12122  prodrbdclem2  12152  efcllemp  12237  ef0lem  12239  efgt0  12263  eftlub  12269  efsep  12270  effsumlt  12271  tanval3ap  12293  efi4p  12296  resin4p  12297  recos4p  12298  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sinltxirr  12340  sin01gt0  12341  cos01gt0  12342  absefib  12350  efieq1re  12351  eirraplem  12356  dvdsdc  12377  dvdscmulr  12399  fsumdvds  12421  dvdslelemd  12422  3dvds  12443  odd2np1lem  12451  odd2np1  12452  flodddiv4  12515  bitsfzo  12534  bitsmod  12535  gcdsupex  12546  gcdsupcl  12547  gcd1  12576  nninfctlemfo  12629  nn0seqcvgd  12631  algcvg  12638  algcvgblem  12639  eucalg  12649  prmind2  12710  qden1elz  12795  dfphi2  12810  phiprm  12813  phimullem  12815  prmdiv  12825  prmdiveq  12826  prm23lt5  12854  pcpre1  12883  pczpre  12888  pcdiv  12893  pc1  12896  pcqdiv  12898  pcexp  12900  pcxnn0cl  12901  pcxcl  12902  pcdvdstr  12918  pc2dvds  12921  sumhashdc  12938  fldivp1  12939  pcfaclem  12940  qexpz  12943  expnprm  12944  prmpwdvds  12946  pockthlem  12947  4sqlem5  12973  4sqlem6  12974  4sqlem11  12992  4sqlem13m  12994  4sqlem19  13000  oddennn  13031  xpct  13035  ennnfonelemj0  13040  ennnfonelemen  13060  ctinfomlemom  13066  omctfn  13082  restid  13351  prdsex  13370  prdsval  13374  prdsbaslemss  13375  prdsbas  13377  imasbas  13408  imasplusg  13409  imasmulr  13410  imasaddfnlemg  13415  xpscf  13448  igsumvalx  13490  gsumsplit1r  13499  gsumprval  13500  gsumfzz  13596  gsumfzcl  13600  prdsgrpd  13710  prdsinvgd  13711  mulgnngsum  13732  mulgnndir  13756  mulgneg2  13761  dvdsrmuld  14129  zsssubrg  14618  znval  14669  znle  14670  znbaslemnn  14672  znf1o  14684  znleval  14686  psrval  14699  restuni2  14920  cnrest2r  14980  lmfss  14987  lmres  14991  lmtopcnp  14993  ispsmet  15066  isxmet2d  15091  ismet2  15097  blfvalps  15128  blex  15130  xblss2  15148  reopnap  15289  divcnap  15308  climcncf  15327  cncfmpt2fcntop  15342  hovera  15390  limcdifap  15405  cnplimcim  15410  cnlimcim  15414  cnlimc  15415  cnlimci  15416  dvbss  15428  dvcnp2cntop  15442  dvcn  15443  dvaddxxbr  15444  dvmulxxbr  15445  dvexp  15454  dveflem  15469  plyval  15475  elply2  15478  plyf  15480  plyss  15481  plyssc  15482  elplyr  15483  plyaddlem1  15490  plymullem1  15491  plyaddlem  15492  plymullem  15493  plyco  15502  plycj  15504  dvply1  15508  reeff1olem  15514  sinperlem  15551  sin2kpi  15554  cos2kpi  15555  sin2pim  15556  cos2pim  15557  cosq14gt0  15575  coseq0q4123  15577  tangtx  15581  abssinper  15589  sinkpi  15590  coskpi  15591  cosq34lt1  15593  logrpap0b  15619  logdivlti  15624  rpcxpsqrtth  15673  rpabscxpbnd  15683  binom4  15722  wilthlem1  15723  0sgm  15728  1sgmprm  15737  1sgm2ppw  15738  mersenne  15740  perfect1  15741  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgslem1  15748  lgsval  15752  lgsfvalg  15753  lgsfcl2  15754  lgsfcl  15756  lgsval2lem  15758  lgsvalmod  15767  lgsneg  15772  lgsdilem  15775  lgsdir2lem3  15778  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgsabs1  15787  lgsprme0  15790  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem0d  15800  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem3  15811  gausslemma2dlem4  15812  gausslemma2dlem5a  15813  gausslemma2dlem5  15814  gausslemma2dlem6  15815  lgseisenlem2  15819  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  lgsquad2lem2  15830  lgsquad2  15831  m1lgs  15833  2lgslem1  15839  2lgslem2  15840  2lgs  15852  2sqlem9  15872  2sqlem10  15873  ushgredgedg  16096  ushgredgedgloop  16098  uhgrspansubgrlem  16146  wlkvtxiedg  16215  wlkvtxiedgg  16216  wlk1walkdom  16229  upgr2wlkdc  16247  clwwlkccatlem  16270  umgrclwwlkge2  16272  clwwlknonmpo  16298  clwwlknonex2lem2  16308  clwwlknonex2  16309  konigsberglem1  16358  2omap  16645  pwle2  16650  pw1nct  16655  nninfsellemdc  16663  nnnninfen  16674  nnnninfex  16675  nninfnfiinf  16676  sbthom  16681  trirec0  16699  apdifflemr  16702  reap0  16714  nconstwlpolem  16721  gfsumval  16732