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  1805  sseqtrid  3274  ssdifin0  3573  uneqdifeqim  3577  unimax  3922  opth  4323  djussxp  4867  iss  5051  relresfld  5258  eldmrexrn  5776  f1oresrab  5800  fmptco  5801  fsn  5807  fnressn  5825  foima2  5875  foeqcnvco  5914  isoini2  5943  relmptopab  6207  ofres  6233  ofco  6237  tposexg  6404  tfrlemisucaccv  6471  tfrlemibex  6475  tfri1dALT  6497  tfrcl  6510  rdgivallem  6527  frecabex  6544  frectfr  6546  frecrdg  6554  pmresg  6823  mapsn  6837  mapsncnv  6842  ixpsnf1o  6883  en1  6951  2dom  6958  enpr2d  6972  en2  6973  mapxpen  7009  phplem4  7016  exmidpw2en  7074  fiintim  7093  sbthlem2  7125  elfir  7140  infglbti  7192  caseinl  7258  caseinr  7259  difinfsnlem  7266  difinfsn  7267  nninfisollemne  7298  exmidfodomrlemim  7379  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  2omotaplemap  7443  archnqq  7604  prarloclemlt  7680  prarloclemlo  7681  prarloclemcalc  7689  recexprlemm  7811  recexprlemex  7824  caucvgprlemm  7855  caucvgprprlemmu  7882  suplocexprlem2b  7901  suplocexprlemmu  7905  suplocexprlemlub  7911  1idsr  7955  recexgt0sr  7960  archsr  7969  caucvgsrlemoffval  7983  caucvgsrlemofff  7984  caucvgsrlemoffres  7987  caucvgsr  7989  ltpsrprg  7990  suplocsrlem  7995  pitonnlem2  8034  pitonn  8035  pitoregt0  8036  pitore  8037  recnnre  8038  axrnegex  8066  nntopi  8081  msqge0  8763  mulge0  8766  recexaplem2  8799  recexap  8800  recgt0  8997  recreclt  9047  nn1m1nn  9128  nn1suc  9129  nnle1eq1  9134  nn1gt1  9144  nnsub  9149  addltmul  9348  nn0le0eq0  9397  elnn0nn  9411  elnnz  9456  elznn0  9461  zlem1lt  9503  zltlem1  9504  elz2  9518  nn0n0n1ge2b  9526  nn0lt2  9528  nn0le2is012  9529  eluzaddi  9749  eluzsubi  9750  uzp1  9756  peano2uzr  9780  nn01to3  9812  qreccl  9837  irrmulap  9843  ltpnf  9976  xaddass2  10066  iccen  10202  fz01en  10249  fzpreddisj  10267  fzsuc2  10275  fseq1p1m1  10290  fseq1m1p1  10291  elfzp1b  10293  fzoss2  10370  fzval3  10410  fzosplitsnm1  10415  fzosplitprm1  10440  flhalf  10522  fldiv4lem1div2uz2  10526  modqmulnn  10564  modqmuladdnn0  10590  frec2uzrand  10627  frecuzrdg0  10635  frecuzrdg0t  10644  frecfzennn  10648  frecfzen2  10649  uzennn  10658  seqeq1  10672  seqp1g  10688  seqclg  10694  seq3m1  10695  monoord2  10708  ser3mono  10709  seqf1oglem1  10741  seqf1oglem2  10742  seqfeq4g  10753  ser0f  10756  exp3vallem  10762  expm1t  10789  expeq0  10792  expubnd  10818  binom3  10879  facndiv  10961  facavg  10968  bcn0  10977  bcnp1n  10981  bcm1k  10982  bcp1nk  10984  bcval5  10985  bcn2  10986  bcp1m1  10987  bcpasc  10988  bcn2m1  10991  hashsng  11020  hashun  11027  hashfz  11043  hashfzo  11044  seq3coll  11064  hash2en  11065  iswrdiz  11078  snopiswrd  11081  ccat1st1st  11172  swrds1  11200  cats1un  11253  wrdind  11254  wrd2ind  11255  swrdccatin1  11257  swrdccat3blem  11271  shftfval  11332  2shfti  11342  resqrexlemf1  11519  abs00ap  11573  sqabs  11593  ltabs  11598  caubnd2  11628  max0addsup  11730  rexico  11732  mulcn2  11823  climaddc1  11840  climmulc2  11842  climsubc1  11843  climsubc2  11844  iserex  11850  climlec2  11852  iser3shft  11857  climcvg1nlem  11860  serf0  11863  sumrbdc  11890  fsumm1  11927  fsump1  11931  fsum00  11973  telfsumo  11977  fsumparts  11981  hashiun  11989  binomlem  11994  binom1dif  11998  bcxmas  12000  isumsplit  12002  isum1p  12003  arisum  12009  arisum2  12010  trireciplem  12011  explecnv  12016  geolim  12022  georeclim  12024  mertenslem2  12047  mertensabs  12048  prodf1f  12054  prodrbdclem2  12084  efcllemp  12169  ef0lem  12171  efgt0  12195  eftlub  12201  efsep  12202  effsumlt  12203  tanval3ap  12225  efi4p  12228  resin4p  12229  recos4p  12230  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  sinltxirr  12272  sin01gt0  12273  cos01gt0  12274  absefib  12282  efieq1re  12283  eirraplem  12288  dvdsdc  12309  dvdscmulr  12331  fsumdvds  12353  dvdslelemd  12354  3dvds  12375  odd2np1lem  12383  odd2np1  12384  flodddiv4  12447  bitsfzo  12466  bitsmod  12467  gcdsupex  12478  gcdsupcl  12479  gcd1  12508  nninfctlemfo  12561  nn0seqcvgd  12563  algcvg  12570  algcvgblem  12571  eucalg  12581  prmind2  12642  qden1elz  12727  dfphi2  12742  phiprm  12745  phimullem  12747  prmdiv  12757  prmdiveq  12758  prm23lt5  12786  pcpre1  12815  pczpre  12820  pcdiv  12825  pc1  12828  pcqdiv  12830  pcexp  12832  pcxnn0cl  12833  pcxcl  12834  pcdvdstr  12850  pc2dvds  12853  sumhashdc  12870  fldivp1  12871  pcfaclem  12872  qexpz  12875  expnprm  12876  prmpwdvds  12878  pockthlem  12879  4sqlem5  12905  4sqlem6  12906  4sqlem11  12924  4sqlem13m  12926  4sqlem19  12932  oddennn  12963  xpct  12967  ennnfonelemj0  12972  ennnfonelemen  12992  ctinfomlemom  12998  omctfn  13014  restid  13283  prdsex  13302  prdsval  13306  prdsbaslemss  13307  prdsbas  13309  imasbas  13340  imasplusg  13341  imasmulr  13342  imasaddfnlemg  13347  xpscf  13380  igsumvalx  13422  gsumsplit1r  13431  gsumprval  13432  gsumfzz  13528  gsumfzcl  13532  prdsgrpd  13642  prdsinvgd  13643  mulgnngsum  13664  mulgnndir  13688  mulgneg2  13693  dvdsrmuld  14060  zsssubrg  14549  znval  14600  znle  14601  znbaslemnn  14603  znf1o  14615  znleval  14617  psrval  14630  restuni2  14851  cnrest2r  14911  lmfss  14918  lmres  14922  lmtopcnp  14924  ispsmet  14997  isxmet2d  15022  ismet2  15028  blfvalps  15059  blex  15061  xblss2  15079  reopnap  15220  divcnap  15239  climcncf  15258  cncfmpt2fcntop  15273  hovera  15321  limcdifap  15336  cnplimcim  15341  cnlimcim  15345  cnlimc  15346  cnlimci  15347  dvbss  15359  dvcnp2cntop  15373  dvcn  15374  dvaddxxbr  15375  dvmulxxbr  15376  dvexp  15385  dveflem  15400  plyval  15406  elply2  15409  plyf  15411  plyss  15412  plyssc  15413  elplyr  15414  plyaddlem1  15421  plymullem1  15422  plyaddlem  15423  plymullem  15424  plyco  15433  plycj  15435  dvply1  15439  reeff1olem  15445  sinperlem  15482  sin2kpi  15485  cos2kpi  15486  sin2pim  15487  cos2pim  15488  cosq14gt0  15506  coseq0q4123  15508  tangtx  15512  abssinper  15520  sinkpi  15521  coskpi  15522  cosq34lt1  15524  logrpap0b  15550  logdivlti  15555  rpcxpsqrtth  15604  rpabscxpbnd  15614  binom4  15653  wilthlem1  15654  0sgm  15659  1sgmprm  15668  1sgm2ppw  15669  mersenne  15671  perfect1  15672  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgslem1  15679  lgsval  15683  lgsfvalg  15684  lgsfcl2  15685  lgsfcl  15687  lgsval2lem  15689  lgsvalmod  15698  lgsneg  15703  lgsdilem  15706  lgsdir2lem3  15709  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsabs1  15718  lgsprme0  15721  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem0d  15731  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem3  15742  gausslemma2dlem4  15743  gausslemma2dlem5a  15744  gausslemma2dlem5  15745  gausslemma2dlem6  15746  lgseisenlem2  15750  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem1  15760  lgsquad2lem2  15761  lgsquad2  15762  m1lgs  15764  2lgslem1  15770  2lgslem2  15771  2lgs  15783  2sqlem9  15803  2sqlem10  15804  ushgredgedg  16024  ushgredgedgloop  16026  wlkvtxiedg  16056  wlkvtxiedgg  16057  wlk1walkdom  16070  2omap  16359  pwle2  16364  pw1nct  16369  nninfsellemdc  16376  nnnninfen  16387  nnnninfex  16388  nninfnfiinf  16389  sbthom  16394  trirec0  16412  apdifflemr  16415  reap0  16426  nconstwlpolem  16433