Theorem sylancl 410

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  sylanblc  412  sylanblrc  413  equveli  1733  sseqtrid  3152  ssdifin0  3449  uneqdifeqim  3453  unimax  3778  opth  4167  djussxp  4692  iss  4873  relresfld  5076  eldmrexrn  5569  f1oresrab  5593  fmptco  5594  fsn  5600  fnressn  5614  foima2  5661  foeqcnvco  5699  isoini2  5728  ofres  6004  ofco  6008  tposexg  6163  tfrlemisucaccv  6230  tfrlemibex  6234  tfri1dALT  6256  tfrcl  6269  rdgivallem  6286  frecabex  6303  frectfr  6305  frecrdg  6313  pmresg  6578  mapsn  6592  mapsncnv  6597  ixpsnf1o  6638  en1  6701  2dom  6707  enpr2d  6719  mapxpen  6750  phplem4  6757  fiintim  6825  sbthlem2  6854  elfir  6869  infglbti  6920  caseinl  6984  caseinr  6985  difinfsnlem  6992  difinfsn  6993  exmidfodomrlemim  7074  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  archnqq  7249  prarloclemlt  7325  prarloclemlo  7326  prarloclemcalc  7334  recexprlemm  7456  recexprlemex  7469  caucvgprlemm  7500  caucvgprprlemmu  7527  suplocexprlem2b  7546  suplocexprlemmu  7550  suplocexprlemlub  7556  1idsr  7600  recexgt0sr  7605  archsr  7614  caucvgsrlemoffval  7628  caucvgsrlemofff  7629  caucvgsrlemoffres  7632  caucvgsr  7634  ltpsrprg  7635  suplocsrlem  7640  pitonnlem2  7679  pitonn  7680  pitoregt0  7681  pitore  7682  recnnre  7683  axrnegex  7711  nntopi  7726  msqge0  8402  mulge0  8405  recexaplem2  8437  recexap  8438  recgt0  8632  recreclt  8682  nn1m1nn  8762  nn1suc  8763  nnle1eq1  8768  nn1gt1  8778  nnsub  8783  addltmul  8980  nn0le0eq0  9029  elnn0nn  9043  elnnz  9088  elznn0  9093  zlem1lt  9134  zltlem1  9135  elz2  9146  nn0n0n1ge2b  9154  nn0lt2  9156  nn0le2is012  9157  eluzaddi  9376  eluzsubi  9377  uzp1  9383  peano2uzr  9407  nn01to3  9436  qreccl  9461  ltpnf  9597  xaddass2  9683  iccen  9819  fz01en  9864  fzpreddisj  9882  fzsuc2  9890  fseq1p1m1  9905  fseq1m1p1  9906  elfzp1b  9908  fzoss2  9980  fzval3  10012  fzosplitsnm1  10017  fzosplitprm1  10042  flhalf  10106  modqmulnn  10146  modqmuladdnn0  10172  frec2uzrand  10209  frecuzrdg0  10217  frecuzrdg0t  10226  frecfzennn  10230  frecfzen2  10231  uzennn  10240  seqeq1  10252  seq3m1  10272  monoord2  10281  ser3mono  10282  ser0f  10319  exp3vallem  10325  expm1t  10352  expeq0  10355  expubnd  10381  binom3  10440  facndiv  10517  facavg  10524  bcn0  10533  bcnp1n  10537  bcm1k  10538  bcp1nk  10540  bcval5  10541  bcn2  10542  bcp1m1  10543  bcpasc  10544  bcn2m1  10547  hashsng  10576  hashun  10583  hashfz  10599  hashfzo  10600  seq3coll  10617  shftfval  10625  2shfti  10635  resqrexlemf1  10812  abs00ap  10866  sqabs  10886  ltabs  10891  caubnd2  10921  max0addsup  11023  rexico  11025  mulcn2  11113  climaddc1  11130  climmulc2  11132  climsubc1  11133  climsubc2  11134  iserex  11140  climlec2  11142  iser3shft  11147  climcvg1nlem  11150  serf0  11153  sumrbdc  11180  fsumm1  11217  fsump1  11221  fsum00  11263  telfsumo  11267  fsumparts  11271  hashiun  11279  binomlem  11284  binom1dif  11288  bcxmas  11290  isumsplit  11292  isum1p  11293  arisum  11299  arisum2  11300  trireciplem  11301  explecnv  11306  geolim  11312  georeclim  11314  mertenslem2  11337  mertensabs  11338  prodf1f  11344  prodrbdclem2  11374  efcllemp  11401  ef0lem  11403  efgt0  11427  eftlub  11433  efsep  11434  effsumlt  11435  tanval3ap  11457  efi4p  11460  resin4p  11461  recos4p  11462  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  cos01gt0  11505  absefib  11513  efieq1re  11514  eirraplem  11519  dvdsdc  11537  dvdscmulr  11558  dvdslelemd  11577  odd2np1lem  11605  odd2np1  11606  flodddiv4  11667  gcdsupex  11682  gcdsupcl  11683  gcd1  11711  nn0seqcvgd  11758  algcvg  11765  algcvgblem  11766  eucalg  11776  prmind2  11837  qden1elz  11919  dfphi2  11932  phiprm  11935  phimullem  11937  oddennn  11941  xpct  11945  ennnfonelemj0  11950  ennnfonelemen  11970  ctinfomlemom  11976  omctfn  11992  restid  12170  restuni2  12385  cnrest2r  12445  lmfss  12452  lmres  12456  lmtopcnp  12458  ispsmet  12531  isxmet2d  12556  ismet2  12562  blfvalps  12593  blex  12595  xblss2  12613  reopnap  12746  divcnap  12763  climcncf  12779  cncfmpt2fcntop  12793  limcdifap  12839  cnplimcim  12844  cnlimcim  12848  cnlimc  12849  cnlimci  12850  dvbss  12862  dvcnp2cntop  12871  dvcn  12872  dvaddxxbr  12873  dvmulxxbr  12874  dvexp  12883  dveflem  12895  reeff1olem  12900  sinperlem  12937  sin2kpi  12940  cos2kpi  12941  sin2pim  12942  cos2pim  12943  cosq14gt0  12961  coseq0q4123  12963  tangtx  12967  abssinper  12975  sinkpi  12976  coskpi  12977  cosq34lt1  12979  logrpap0b  13005  logdivlti  13010  rpcxpsqrtth  13058  rpabscxpbnd  13067  pwle2  13366  pw1nct  13371  nninfsellemdc  13381  sbthom  13396  trirec0  13412  apdifflemr  13415