Theorem sylancl 392

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

Syntax hints:   -> wi 4   /\ wa 97

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

This theorem is referenced by:  equveli  1642  syl5sseq  2993  ssdifin0  3304  uneqdifeqim  3308  unimax  3614  opth  3974  djussxp  4481  iss  4654  relresfld  4847  eldmrexrn  5308  f1oresrab  5329  fmptco  5330  fsn  5335  fnressn  5349  foeqcnvco  5430  isoini2  5458  ofres  5725  ofco  5729  tposexg  5873  tfrlemisucaccv  5939  tfrlemibex  5943  rdgivallem  5968  frecabex  5984  frectfr  5985  frecrdg  5992  en1  6279  2dom  6285  phplem4  6318  archnqq  6515  prarloclemlt  6591  prarloclemlo  6592  prarloclemcalc  6600  recexprlemm  6722  recexprlemex  6735  caucvgprlemm  6766  caucvgprprlemmu  6793  1idsr  6853  recexgt0sr  6858  archsr  6866  caucvgsrlemoffval  6880  caucvgsrlemofff  6881  caucvgsrlemoffres  6884  caucvgsr  6886  pitonnlem2  6923  pitonn  6924  pitoregt0  6925  pitore  6926  recnnre  6927  axrnegex  6953  nntopi  6968  msqge0  7607  mulge0  7610  recexaplem2  7633  recexap  7634  recgt0  7816  recreclt  7866  nn1m1nn  7932  nn1suc  7933  nnle1eq1  7938  nn1gt1  7947  nnsub  7952  addltmul  8161  nn0le0eq0  8210  elnn0nn  8224  elnnz  8255  elznn0  8260  zlem1lt  8300  zltlem1  8301  elz2  8312  nn0n0n1ge2b  8320  nn0lt2  8322  eluzaddi  8499  eluzsubi  8500  uzp1  8506  peano2uzr  8528  nn01to3  8552  qreccl  8576  ltpnf  8702  fz01en  8917  fzpreddisj  8933  fzsuc2  8941  fseq1p1m1  8956  fseq1m1p1  8957  elfzp1b  8959  fzoss2  9028  fzval3  9060  fzosplitsnm1  9065  fzosplitprm1  9090  flhalf  9144  modqmulnn  9184  frec2uzrand  9191  frecuzrdgrom  9196  frecuzrdg0  9200  frecfzennn  9203  frecfzen2  9204  iseqeq1  9214  iseqm1  9227  monoord2  9236  isermono  9237  iser0f  9251  expm1t  9283  expeq0  9286  expubnd  9311  binom3  9366  shftfval  9422  2shfti  9432  resqrexlemf1  9606  abs00ap  9660  abs00  9662  sqabs  9678  ltabs  9683  caubnd2  9713  mulcn2  9833  climaddc1  9849  climmulc2  9851  climsubc1  9852  climsubc2  9853  iiserex  9859  climlec2  9861  climcvg1nlem  9868  serif0  9871  nn0seqcvgd  9880  ialgcvg  9887  algcvgblem  9888