Theorem sylancl 404

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  sylanblc  406  sylanblrc  407  equveli  1682  syl5sseq  3047  ssdifin0  3324  uneqdifeqim  3328  unimax  3635  opth  3992  djussxp  4499  iss  4674  relresfld  4867  eldmrexrn  5329  f1oresrab  5350  fmptco  5351  fsn  5356  fnressn  5370  foeqcnvco  5450  isoini2  5478  ofres  5745  ofco  5749  tposexg  5896  tfrlemisucaccv  5962  tfrlemibex  5966  rdgivallem  5991  frecabex  6007  frectfr  6008  frecrdg  6015  en1  6302  2dom  6308  phplem4  6341  infglbti  6438  archnqq  6607  prarloclemlt  6683  prarloclemlo  6684  prarloclemcalc  6692  recexprlemm  6814  recexprlemex  6827  caucvgprlemm  6858  caucvgprprlemmu  6885  1idsr  6945  recexgt0sr  6950  archsr  6958  caucvgsrlemoffval  6972  caucvgsrlemofff  6973  caucvgsrlemoffres  6976  caucvgsr  6978  pitonnlem2  7015  pitonn  7016  pitoregt0  7017  pitore  7018  recnnre  7019  axrnegex  7045  nntopi  7060  msqge0  7716  mulge0  7719  recexaplem2  7742  recexap  7743  recgt0  7928  recreclt  7978  nn1m1nn  8057  nn1suc  8058  nnle1eq1  8063  nn1gt1  8072  nnsub  8077  addltmul  8267  nn0le0eq0  8316  elnn0nn  8330  elnnz  8361  elznn0  8366  zlem1lt  8407  zltlem1  8408  elz2  8419  nn0n0n1ge2b  8427  nn0lt2  8429  eluzaddi  8645  eluzsubi  8646  uzp1  8652  peano2uzr  8673  nn01to3  8702  qreccl  8727  ltpnf  8856  fz01en  9072  fzpreddisj  9088  fzsuc2  9096  fseq1p1m1  9111  fseq1m1p1  9112  elfzp1b  9114  fzoss2  9181  fzval3  9213  fzosplitsnm1  9218  fzosplitprm1  9243  flhalf  9304  modqmulnn  9344  modqmuladdnn0  9370  frec2uzrand  9407  frecuzrdgrom  9412  frecuzrdg0  9416  frecfzennn  9419  frecfzen2  9420  iseqeq1  9434  iseqm1  9447  monoord2  9456  isermono  9457  iser0f  9472  expm1t  9504  expeq0  9507  expubnd  9533  binom3  9590  facndiv  9666  facavg  9673  bcn0  9682  bcnp1n  9686  bcm1k  9687  bcp1nk  9689  ibcval5  9690  bcn2  9691  bcp1m1  9692  bcpasc  9693  bcn2m1  9696  shftfval  9709  2shfti  9719  resqrexlemf1  9894  abs00ap  9948  abs00  9950  sqabs  9968  ltabs  9973  caubnd2  10003  max0addsup  10105  rexico  10107  mulcn2  10151  climaddc1  10167  climmulc2  10169  climsubc1  10170  climsubc2  10171  iiserex  10177  climlec2  10179  climcvg1nlem  10186  serif0  10189  dvdsdc  10203  dvdscmulr  10224  dvdslelemd  10243  odd2np1lem  10271  odd2np1  10272  flodddiv4  10334  gcdsupex  10349  gcdsupcl  10350  gcd1  10378  nn0seqcvgd  10423  ialgcvg  10430  algcvgblem  10431  eucialg  10441  prmind2  10502