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

Theorem sylancl 404
Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylancl.1 (𝜑𝜓)
sylancl.2 𝜒
sylancl.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
sylancl (𝜑𝜃)

Proof of Theorem sylancl
StepHypRef Expression
1 sylancl.1 . 2 (𝜑𝜓)
2 sylancl.2 . . 3 𝜒
32a1i 9 . 2 (𝜑𝜒)
4 sylancl.3 . 2 ((𝜓𝜒) → 𝜃)
51, 3, 4syl2anc 403 1 (𝜑𝜃)
Colors of variables: wff set class
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  1684  syl5sseq  3057  ssdifin0  3341  uneqdifeqim  3345  unimax  3656  opth  4021  djussxp  4530  iss  4705  relresfld  4898  eldmrexrn  5362  f1oresrab  5383  fmptco  5384  fsn  5389  fnressn  5403  foeqcnvco  5483  isoini2  5511  ofres  5778  ofco  5782  tposexg  5929  tfrlemisucaccv  5996  tfrlemibex  6000  tfri1dALT  6022  tfrcl  6035  rdgivallem  6052  frecabex  6069  frectfr  6071  frecrdg  6079  en1  6369  2dom  6375  phplem4  6413  infglbti  6534  archnqq  6746  prarloclemlt  6822  prarloclemlo  6823  prarloclemcalc  6831  recexprlemm  6953  recexprlemex  6966  caucvgprlemm  6997  caucvgprprlemmu  7024  1idsr  7084  recexgt0sr  7089  archsr  7097  caucvgsrlemoffval  7111  caucvgsrlemofff  7112  caucvgsrlemoffres  7115  caucvgsr  7117  pitonnlem2  7154  pitonn  7155  pitoregt0  7156  pitore  7157  recnnre  7158  axrnegex  7184  nntopi  7199  msqge0  7860  mulge0  7863  recexaplem2  7886  recexap  7887  recgt0  8072  recreclt  8122  nn1m1nn  8201  nn1suc  8202  nnle1eq1  8207  nn1gt1  8216  nnsub  8221  addltmul  8411  nn0le0eq0  8460  elnn0nn  8474  elnnz  8519  elznn0  8524  zlem1lt  8565  zltlem1  8566  elz2  8577  nn0n0n1ge2b  8585  nn0lt2  8587  eluzaddi  8803  eluzsubi  8804  uzp1  8810  peano2uzr  8831  nn01to3  8860  qreccl  8885  ltpnf  9009  fz01en  9225  fzpreddisj  9241  fzsuc2  9249  fseq1p1m1  9264  fseq1m1p1  9265  elfzp1b  9267  fzoss2  9335  fzval3  9367  fzosplitsnm1  9372  fzosplitprm1  9397  flhalf  9461  modqmulnn  9501  modqmuladdnn0  9527  frec2uzrand  9564  frecuzrdg0  9572  frecuzrdg0t  9581  frecfzennn  9585  frecfzen2  9586  iseqeq1  9601  iseqm1  9620  monoord2  9629  isermono  9630  iser0f  9646  expm1t  9678  expeq0  9681  expubnd  9707  binom3  9764  facndiv  9840  facavg  9847  bcn0  9856  bcnp1n  9860  bcm1k  9861  bcp1nk  9863  ibcval5  9864  bcn2  9865  bcp1m1  9866  bcpasc  9867  bcn2m1  9870  hashsng  9899  hashun  9906  hashfz  9922  hashfzo  9923  shftfval  9935  2shfti  9945  resqrexlemf1  10120  abs00ap  10174  abs00  10176  sqabs  10194  ltabs  10199  caubnd2  10229  max0addsup  10331  rexico  10333  mulcn2  10377  climaddc1  10393  climmulc2  10395  climsubc1  10396  climsubc2  10397  iiserex  10403  climlec2  10405  climcvg1nlem  10412  serif0  10415  isumrb  10427  dvdsdc  10436  dvdscmulr  10457  dvdslelemd  10476  odd2np1lem  10504  odd2np1  10505  flodddiv4  10566  gcdsupex  10581  gcdsupcl  10582  gcd1  10610  nn0seqcvgd  10655  ialgcvg  10662  algcvgblem  10663  eucialg  10673  prmind2  10734  qden1elz  10815  dfphi2  10828  phiprm  10831  phimullem  10833  oddennn  10837  xpct  10841
  Copyright terms: Public domain W3C validator