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  1783  sseqtrid  3251  ssdifin0  3550  uneqdifeqim  3554  unimax  3898  opth  4299  djussxp  4841  iss  5024  relresfld  5231  eldmrexrn  5744  f1oresrab  5768  fmptco  5769  fsn  5775  fnressn  5793  foima2  5843  foeqcnvco  5882  isoini2  5911  ofres  6196  ofco  6200  tposexg  6367  tfrlemisucaccv  6434  tfrlemibex  6438  tfri1dALT  6460  tfrcl  6473  rdgivallem  6490  frecabex  6507  frectfr  6509  frecrdg  6517  pmresg  6786  mapsn  6800  mapsncnv  6805  ixpsnf1o  6846  en1  6914  2dom  6921  enpr2d  6935  en2  6936  mapxpen  6970  phplem4  6977  exmidpw2en  7035  fiintim  7054  sbthlem2  7086  elfir  7101  infglbti  7153  caseinl  7219  caseinr  7220  difinfsnlem  7227  difinfsn  7228  nninfisollemne  7259  exmidfodomrlemim  7340  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  2omotaplemap  7404  archnqq  7565  prarloclemlt  7641  prarloclemlo  7642  prarloclemcalc  7650  recexprlemm  7772  recexprlemex  7785  caucvgprlemm  7816  caucvgprprlemmu  7843  suplocexprlem2b  7862  suplocexprlemmu  7866  suplocexprlemlub  7872  1idsr  7916  recexgt0sr  7921  archsr  7930  caucvgsrlemoffval  7944  caucvgsrlemofff  7945  caucvgsrlemoffres  7948  caucvgsr  7950  ltpsrprg  7951  suplocsrlem  7956  pitonnlem2  7995  pitonn  7996  pitoregt0  7997  pitore  7998  recnnre  7999  axrnegex  8027  nntopi  8042  msqge0  8724  mulge0  8727  recexaplem2  8760  recexap  8761  recgt0  8958  recreclt  9008  nn1m1nn  9089  nn1suc  9090  nnle1eq1  9095  nn1gt1  9105  nnsub  9110  addltmul  9309  nn0le0eq0  9358  elnn0nn  9372  elnnz  9417  elznn0  9422  zlem1lt  9464  zltlem1  9465  elz2  9479  nn0n0n1ge2b  9487  nn0lt2  9489  nn0le2is012  9490  eluzaddi  9710  eluzsubi  9711  uzp1  9717  peano2uzr  9741  nn01to3  9773  qreccl  9798  irrmulap  9804  ltpnf  9937  xaddass2  10027  iccen  10163  fz01en  10210  fzpreddisj  10228  fzsuc2  10236  fseq1p1m1  10251  fseq1m1p1  10252  elfzp1b  10254  fzoss2  10331  fzval3  10370  fzosplitsnm1  10375  fzosplitprm1  10400  flhalf  10482  fldiv4lem1div2uz2  10486  modqmulnn  10524  modqmuladdnn0  10550  frec2uzrand  10587  frecuzrdg0  10595  frecuzrdg0t  10604  frecfzennn  10608  frecfzen2  10609  uzennn  10618  seqeq1  10632  seqp1g  10648  seqclg  10654  seq3m1  10655  monoord2  10668  ser3mono  10669  seqf1oglem1  10701  seqf1oglem2  10702  seqfeq4g  10713  ser0f  10716  exp3vallem  10722  expm1t  10749  expeq0  10752  expubnd  10778  binom3  10839  facndiv  10921  facavg  10928  bcn0  10937  bcnp1n  10941  bcm1k  10942  bcp1nk  10944  bcval5  10945  bcn2  10946  bcp1m1  10947  bcpasc  10948  bcn2m1  10951  hashsng  10980  hashun  10987  hashfz  11003  hashfzo  11004  seq3coll  11024  hash2en  11025  iswrdiz  11038  snopiswrd  11041  ccat1st1st  11131  swrds1  11159  cats1un  11212  wrdind  11213  wrd2ind  11214  swrdccatin1  11216  swrdccat3blem  11230  shftfval  11247  2shfti  11257  resqrexlemf1  11434  abs00ap  11488  sqabs  11508  ltabs  11513  caubnd2  11543  max0addsup  11645  rexico  11647  mulcn2  11738  climaddc1  11755  climmulc2  11757  climsubc1  11758  climsubc2  11759  iserex  11765  climlec2  11767  iser3shft  11772  climcvg1nlem  11775  serf0  11778  sumrbdc  11805  fsumm1  11842  fsump1  11846  fsum00  11888  telfsumo  11892  fsumparts  11896  hashiun  11904  binomlem  11909  binom1dif  11913  bcxmas  11915  isumsplit  11917  isum1p  11918  arisum  11924  arisum2  11925  trireciplem  11926  explecnv  11931  geolim  11937  georeclim  11939  mertenslem2  11962  mertensabs  11963  prodf1f  11969  prodrbdclem2  11999  efcllemp  12084  ef0lem  12086  efgt0  12110  eftlub  12116  efsep  12117  effsumlt  12118  tanval3ap  12140  efi4p  12143  resin4p  12144  recos4p  12145  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  sinltxirr  12187  sin01gt0  12188  cos01gt0  12189  absefib  12197  efieq1re  12198  eirraplem  12203  dvdsdc  12224  dvdscmulr  12246  fsumdvds  12268  dvdslelemd  12269  3dvds  12290  odd2np1lem  12298  odd2np1  12299  flodddiv4  12362  bitsfzo  12381  bitsmod  12382  gcdsupex  12393  gcdsupcl  12394  gcd1  12423  nninfctlemfo  12476  nn0seqcvgd  12478  algcvg  12485  algcvgblem  12486  eucalg  12496  prmind2  12557  qden1elz  12642  dfphi2  12657  phiprm  12660  phimullem  12662  prmdiv  12672  prmdiveq  12673  prm23lt5  12701  pcpre1  12730  pczpre  12735  pcdiv  12740  pc1  12743  pcqdiv  12745  pcexp  12747  pcxnn0cl  12748  pcxcl  12749  pcdvdstr  12765  pc2dvds  12768  sumhashdc  12785  fldivp1  12786  pcfaclem  12787  qexpz  12790  expnprm  12791  prmpwdvds  12793  pockthlem  12794  4sqlem5  12820  4sqlem6  12821  4sqlem11  12839  4sqlem13m  12841  4sqlem19  12847  oddennn  12878  xpct  12882  ennnfonelemj0  12887  ennnfonelemen  12907  ctinfomlemom  12913  omctfn  12929  restid  13197  prdsex  13216  prdsval  13220  prdsbaslemss  13221  prdsbas  13223  imasbas  13254  imasplusg  13255  imasmulr  13256  imasaddfnlemg  13261  xpscf  13294  igsumvalx  13336  gsumsplit1r  13345  gsumprval  13346  gsumfzz  13442  gsumfzcl  13446  prdsgrpd  13556  prdsinvgd  13557  mulgnngsum  13578  mulgnndir  13602  mulgneg2  13607  dvdsrmuld  13973  zsssubrg  14462  znval  14513  znle  14514  znbaslemnn  14516  znf1o  14528  znleval  14530  psrval  14543  restuni2  14764  cnrest2r  14824  lmfss  14831  lmres  14835  lmtopcnp  14837  ispsmet  14910  isxmet2d  14935  ismet2  14941  blfvalps  14972  blex  14974  xblss2  14992  reopnap  15133  divcnap  15152  climcncf  15171  cncfmpt2fcntop  15186  hovera  15234  limcdifap  15249  cnplimcim  15254  cnlimcim  15258  cnlimc  15259  cnlimci  15260  dvbss  15272  dvcnp2cntop  15286  dvcn  15287  dvaddxxbr  15288  dvmulxxbr  15289  dvexp  15298  dveflem  15313  plyval  15319  elply2  15322  plyf  15324  plyss  15325  plyssc  15326  elplyr  15327  plyaddlem1  15334  plymullem1  15335  plyaddlem  15336  plymullem  15337  plyco  15346  plycj  15348  dvply1  15352  reeff1olem  15358  sinperlem  15395  sin2kpi  15398  cos2kpi  15399  sin2pim  15400  cos2pim  15401  cosq14gt0  15419  coseq0q4123  15421  tangtx  15425  abssinper  15433  sinkpi  15434  coskpi  15435  cosq34lt1  15437  logrpap0b  15463  logdivlti  15468  rpcxpsqrtth  15517  rpabscxpbnd  15527  binom4  15566  wilthlem1  15567  0sgm  15572  1sgmprm  15581  1sgm2ppw  15582  mersenne  15584  perfect1  15585  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgslem1  15592  lgsval  15596  lgsfvalg  15597  lgsfcl2  15598  lgsfcl  15600  lgsval2lem  15602  lgsvalmod  15611  lgsneg  15616  lgsdilem  15619  lgsdir2lem3  15622  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsabs1  15631  lgsprme0  15634  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem0d  15644  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem3  15655  gausslemma2dlem4  15656  gausslemma2dlem5a  15657  gausslemma2dlem5  15658  gausslemma2dlem6  15659  lgseisenlem2  15663  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  lgsquad2lem2  15674  lgsquad2  15675  m1lgs  15677  2lgslem1  15683  2lgslem2  15684  2lgs  15696  2sqlem9  15716  2sqlem10  15717  2omap  16132  pwle2  16137  pw1nct  16142  nninfsellemdc  16149  nnnninfen  16160  nnnninfex  16161  nninfnfiinf  16162  sbthom  16167  trirec0  16185  apdifflemr  16188  reap0  16199  nconstwlpolem  16206