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  1782  sseqtrid  3243  ssdifin0  3542  uneqdifeqim  3546  unimax  3884  opth  4281  djussxp  4823  iss  5005  relresfld  5212  eldmrexrn  5721  f1oresrab  5745  fmptco  5746  fsn  5752  fnressn  5770  foima2  5820  foeqcnvco  5859  isoini2  5888  ofres  6173  ofco  6177  tposexg  6344  tfrlemisucaccv  6411  tfrlemibex  6415  tfri1dALT  6437  tfrcl  6450  rdgivallem  6467  frecabex  6484  frectfr  6486  frecrdg  6494  pmresg  6763  mapsn  6777  mapsncnv  6782  ixpsnf1o  6823  en1  6891  2dom  6897  enpr2d  6911  en2  6912  mapxpen  6945  phplem4  6952  exmidpw2en  7009  fiintim  7028  sbthlem2  7060  elfir  7075  infglbti  7127  caseinl  7193  caseinr  7194  difinfsnlem  7201  difinfsn  7202  nninfisollemne  7233  exmidfodomrlemim  7309  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  2omotaplemap  7369  archnqq  7530  prarloclemlt  7606  prarloclemlo  7607  prarloclemcalc  7615  recexprlemm  7737  recexprlemex  7750  caucvgprlemm  7781  caucvgprprlemmu  7808  suplocexprlem2b  7827  suplocexprlemmu  7831  suplocexprlemlub  7837  1idsr  7881  recexgt0sr  7886  archsr  7895  caucvgsrlemoffval  7909  caucvgsrlemofff  7910  caucvgsrlemoffres  7913  caucvgsr  7915  ltpsrprg  7916  suplocsrlem  7921  pitonnlem2  7960  pitonn  7961  pitoregt0  7962  pitore  7963  recnnre  7964  axrnegex  7992  nntopi  8007  msqge0  8689  mulge0  8692  recexaplem2  8725  recexap  8726  recgt0  8923  recreclt  8973  nn1m1nn  9054  nn1suc  9055  nnle1eq1  9060  nn1gt1  9070  nnsub  9075  addltmul  9274  nn0le0eq0  9323  elnn0nn  9337  elnnz  9382  elznn0  9387  zlem1lt  9429  zltlem1  9430  elz2  9444  nn0n0n1ge2b  9452  nn0lt2  9454  nn0le2is012  9455  eluzaddi  9675  eluzsubi  9676  uzp1  9682  peano2uzr  9706  nn01to3  9738  qreccl  9763  irrmulap  9769  ltpnf  9902  xaddass2  9992  iccen  10128  fz01en  10175  fzpreddisj  10193  fzsuc2  10201  fseq1p1m1  10216  fseq1m1p1  10217  elfzp1b  10219  fzoss2  10296  fzval3  10333  fzosplitsnm1  10338  fzosplitprm1  10363  flhalf  10445  fldiv4lem1div2uz2  10449  modqmulnn  10487  modqmuladdnn0  10513  frec2uzrand  10550  frecuzrdg0  10558  frecuzrdg0t  10567  frecfzennn  10571  frecfzen2  10572  uzennn  10581  seqeq1  10595  seqp1g  10611  seqclg  10617  seq3m1  10618  monoord2  10631  ser3mono  10632  seqf1oglem1  10664  seqf1oglem2  10665  seqfeq4g  10676  ser0f  10679  exp3vallem  10685  expm1t  10712  expeq0  10715  expubnd  10741  binom3  10802  facndiv  10884  facavg  10891  bcn0  10900  bcnp1n  10904  bcm1k  10905  bcp1nk  10907  bcval5  10908  bcn2  10909  bcp1m1  10910  bcpasc  10911  bcn2m1  10914  hashsng  10943  hashun  10950  hashfz  10966  hashfzo  10967  seq3coll  10987  hash2en  10988  iswrdiz  11001  snopiswrd  11004  ccat1st1st  11093  swrds1  11121  shftfval  11132  2shfti  11142  resqrexlemf1  11319  abs00ap  11373  sqabs  11393  ltabs  11398  caubnd2  11428  max0addsup  11530  rexico  11532  mulcn2  11623  climaddc1  11640  climmulc2  11642  climsubc1  11643  climsubc2  11644  iserex  11650  climlec2  11652  iser3shft  11657  climcvg1nlem  11660  serf0  11663  sumrbdc  11690  fsumm1  11727  fsump1  11731  fsum00  11773  telfsumo  11777  fsumparts  11781  hashiun  11789  binomlem  11794  binom1dif  11798  bcxmas  11800  isumsplit  11802  isum1p  11803  arisum  11809  arisum2  11810  trireciplem  11811  explecnv  11816  geolim  11822  georeclim  11824  mertenslem2  11847  mertensabs  11848  prodf1f  11854  prodrbdclem2  11884  efcllemp  11969  ef0lem  11971  efgt0  11995  eftlub  12001  efsep  12002  effsumlt  12003  tanval3ap  12025  efi4p  12028  resin4p  12029  recos4p  12030  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  sinltxirr  12072  sin01gt0  12073  cos01gt0  12074  absefib  12082  efieq1re  12083  eirraplem  12088  dvdsdc  12109  dvdscmulr  12131  fsumdvds  12153  dvdslelemd  12154  3dvds  12175  odd2np1lem  12183  odd2np1  12184  flodddiv4  12247  bitsfzo  12266  bitsmod  12267  gcdsupex  12278  gcdsupcl  12279  gcd1  12308  nninfctlemfo  12361  nn0seqcvgd  12363  algcvg  12370  algcvgblem  12371  eucalg  12381  prmind2  12442  qden1elz  12527  dfphi2  12542  phiprm  12545  phimullem  12547  prmdiv  12557  prmdiveq  12558  prm23lt5  12586  pcpre1  12615  pczpre  12620  pcdiv  12625  pc1  12628  pcqdiv  12630  pcexp  12632  pcxnn0cl  12633  pcxcl  12634  pcdvdstr  12650  pc2dvds  12653  sumhashdc  12670  fldivp1  12671  pcfaclem  12672  qexpz  12675  expnprm  12676  prmpwdvds  12678  pockthlem  12679  4sqlem5  12705  4sqlem6  12706  4sqlem11  12724  4sqlem13m  12726  4sqlem19  12732  oddennn  12763  xpct  12767  ennnfonelemj0  12772  ennnfonelemen  12792  ctinfomlemom  12798  omctfn  12814  restid  13082  prdsex  13101  prdsval  13105  prdsbaslemss  13106  prdsbas  13108  imasbas  13139  imasplusg  13140  imasmulr  13141  imasaddfnlemg  13146  xpscf  13179  igsumvalx  13221  gsumsplit1r  13230  gsumprval  13231  gsumfzz  13327  gsumfzcl  13331  prdsgrpd  13441  prdsinvgd  13442  mulgnngsum  13463  mulgnndir  13487  mulgneg2  13492  dvdsrmuld  13858  zsssubrg  14347  znval  14398  znle  14399  znbaslemnn  14401  znf1o  14413  znleval  14415  psrval  14428  restuni2  14649  cnrest2r  14709  lmfss  14716  lmres  14720  lmtopcnp  14722  ispsmet  14795  isxmet2d  14820  ismet2  14826  blfvalps  14857  blex  14859  xblss2  14877  reopnap  15018  divcnap  15037  climcncf  15056  cncfmpt2fcntop  15071  hovera  15119  limcdifap  15134  cnplimcim  15139  cnlimcim  15143  cnlimc  15144  cnlimci  15145  dvbss  15157  dvcnp2cntop  15171  dvcn  15172  dvaddxxbr  15173  dvmulxxbr  15174  dvexp  15183  dveflem  15198  plyval  15204  elply2  15207  plyf  15209  plyss  15210  plyssc  15211  elplyr  15212  plyaddlem1  15219  plymullem1  15220  plyaddlem  15221  plymullem  15222  plyco  15231  plycj  15233  dvply1  15237  reeff1olem  15243  sinperlem  15280  sin2kpi  15283  cos2kpi  15284  sin2pim  15285  cos2pim  15286  cosq14gt0  15304  coseq0q4123  15306  tangtx  15310  abssinper  15318  sinkpi  15319  coskpi  15320  cosq34lt1  15322  logrpap0b  15348  logdivlti  15353  rpcxpsqrtth  15402  rpabscxpbnd  15412  binom4  15451  wilthlem1  15452  0sgm  15457  1sgmprm  15466  1sgm2ppw  15467  mersenne  15469  perfect1  15470  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgslem1  15477  lgsval  15481  lgsfvalg  15482  lgsfcl2  15483  lgsfcl  15485  lgsval2lem  15487  lgsvalmod  15496  lgsneg  15501  lgsdilem  15504  lgsdir2lem3  15507  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsabs1  15516  lgsprme0  15519  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem0d  15529  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem3  15540  gausslemma2dlem4  15541  gausslemma2dlem5a  15542  gausslemma2dlem5  15543  gausslemma2dlem6  15544  lgseisenlem2  15548  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem1  15558  lgsquad2lem2  15559  lgsquad2  15560  m1lgs  15562  2lgslem1  15568  2lgslem2  15569  2lgs  15581  2sqlem9  15601  2sqlem10  15602  2omap  15932  pwle2  15935  pw1nct  15940  nninfsellemdc  15947  nnnninfen  15958  nnnninfex  15959  nninfnfiinf  15960  sbthom  15965  trirec0  15983  apdifflemr  15986  reap0  15997  nconstwlpolem  16004