ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylancl Unicode version

Theorem sylancl 398
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
StepHypRef Expression
1 sylancl.1 . 2  |-  ( ph  ->  ps )
2 sylancl.2 . . 3  |-  ch
32a1i 9 . 2  |-  ( ph  ->  ch )
4 sylancl.3 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 3, 4syl2anc 397 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  sylanblc  400  sylanblrc  401  equveli  1658  syl5sseq  3021  ssdifin0  3332  uneqdifeqim  3336  unimax  3642  opth  4002  djussxp  4509  iss  4682  relresfld  4875  eldmrexrn  5336  f1oresrab  5357  fmptco  5358  fsn  5363  fnressn  5377  foeqcnvco  5458  isoini2  5486  ofres  5753  ofco  5757  tposexg  5904  tfrlemisucaccv  5970  tfrlemibex  5974  rdgivallem  5999  frecabex  6015  frectfr  6016  frecrdg  6023  en1  6310  2dom  6316  phplem4  6349  archnqq  6573  prarloclemlt  6649  prarloclemlo  6650  prarloclemcalc  6658  recexprlemm  6780  recexprlemex  6793  caucvgprlemm  6824  caucvgprprlemmu  6851  1idsr  6911  recexgt0sr  6916  archsr  6924  caucvgsrlemoffval  6938  caucvgsrlemofff  6939  caucvgsrlemoffres  6942  caucvgsr  6944  pitonnlem2  6981  pitonn  6982  pitoregt0  6983  pitore  6984  recnnre  6985  axrnegex  7011  nntopi  7026  msqge0  7681  mulge0  7684  recexaplem2  7707  recexap  7708  recgt0  7891  recreclt  7941  nn1m1nn  8008  nn1suc  8009  nnle1eq1  8014  nn1gt1  8023  nnsub  8028  addltmul  8218  nn0le0eq0  8267  elnn0nn  8281  elnnz  8312  elznn0  8317  zlem1lt  8358  zltlem1  8359  elz2  8370  nn0n0n1ge2b  8378  nn0lt2  8380  eluzaddi  8595  eluzsubi  8596  uzp1  8602  peano2uzr  8624  nn01to3  8649  qreccl  8674  ltpnf  8803  fz01en  9019  fzpreddisj  9035  fzsuc2  9043  fseq1p1m1  9058  fseq1m1p1  9059  elfzp1b  9061  fzoss2  9130  fzval3  9162  fzosplitsnm1  9167  fzosplitprm1  9192  flhalf  9252  modqmulnn  9292  modqmuladdnn0  9318  frec2uzrand  9355  frecuzrdgrom  9360  frecuzrdg0  9364  frecfzennn  9367  frecfzen2  9368  iseqeq1  9378  iseqm1  9391  monoord2  9400  isermono  9401  iser0f  9416  expm1t  9448  expeq0  9451  expubnd  9477  binom3  9534  facndiv  9607  facavg  9614  bcn0  9623  bcnp1n  9627  bcm1k  9628  bcp1nk  9630  ibcval5  9631  bcn2  9632  bcp1m1  9633  bcpasc  9634  bcn2m1  9637  shftfval  9650  2shfti  9660  resqrexlemf1  9835  abs00ap  9889  abs00  9891  sqabs  9909  ltabs  9914  caubnd2  9944  mulcn2  10064  climaddc1  10080  climmulc2  10082  climsubc1  10083  climsubc2  10084  iiserex  10090  climlec2  10092  climcvg1nlem  10099  serif0  10102  dvdsdc  10116  dvdscmulr  10136  dvdslelemd  10155  odd2np1lem  10183  odd2np1  10184  flodddiv4  10246  nn0seqcvgd  10263  ialgcvg  10270  algcvgblem  10271
  Copyright terms: Public domain W3C validator