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

Theorem sylancl 409
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 408 1  |-  ( ph  ->  th )
Colors of variables: wff set class
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  411  sylanblrc  412  equveli  1717  sseqtrid  3117  ssdifin0  3414  uneqdifeqim  3418  unimax  3740  opth  4129  djussxp  4654  iss  4835  relresfld  5038  eldmrexrn  5529  f1oresrab  5553  fmptco  5554  fsn  5560  fnressn  5574  foima2  5621  foeqcnvco  5659  isoini2  5688  ofres  5964  ofco  5968  tposexg  6123  tfrlemisucaccv  6190  tfrlemibex  6194  tfri1dALT  6216  tfrcl  6229  rdgivallem  6246  frecabex  6263  frectfr  6265  frecrdg  6273  pmresg  6538  mapsn  6552  mapsncnv  6557  ixpsnf1o  6598  en1  6661  2dom  6667  enpr2d  6679  mapxpen  6710  phplem4  6717  fiintim  6785  sbthlem2  6814  elfir  6829  infglbti  6880  caseinl  6944  caseinr  6945  difinfsnlem  6952  difinfsn  6953  exmidfodomrlemim  7025  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  archnqq  7193  prarloclemlt  7269  prarloclemlo  7270  prarloclemcalc  7278  recexprlemm  7400  recexprlemex  7413  caucvgprlemm  7444  caucvgprprlemmu  7471  suplocexprlem2b  7490  suplocexprlemmu  7494  suplocexprlemlub  7500  1idsr  7544  recexgt0sr  7549  archsr  7558  caucvgsrlemoffval  7572  caucvgsrlemofff  7573  caucvgsrlemoffres  7576  caucvgsr  7578  ltpsrprg  7579  suplocsrlem  7584  pitonnlem2  7623  pitonn  7624  pitoregt0  7625  pitore  7626  recnnre  7627  axrnegex  7655  nntopi  7670  msqge0  8345  mulge0  8348  recexaplem2  8380  recexap  8381  recgt0  8572  recreclt  8622  nn1m1nn  8702  nn1suc  8703  nnle1eq1  8708  nn1gt1  8718  nnsub  8723  addltmul  8914  nn0le0eq0  8963  elnn0nn  8977  elnnz  9022  elznn0  9027  zlem1lt  9068  zltlem1  9069  elz2  9080  nn0n0n1ge2b  9088  nn0lt2  9090  nn0le2is012  9091  eluzaddi  9308  eluzsubi  9309  uzp1  9315  peano2uzr  9336  nn01to3  9365  qreccl  9390  ltpnf  9522  xaddass2  9608  fz01en  9788  fzpreddisj  9806  fzsuc2  9814  fseq1p1m1  9829  fseq1m1p1  9830  elfzp1b  9832  fzoss2  9904  fzval3  9936  fzosplitsnm1  9941  fzosplitprm1  9966  flhalf  10030  modqmulnn  10070  modqmuladdnn0  10096  frec2uzrand  10133  frecuzrdg0  10141  frecuzrdg0t  10150  frecfzennn  10154  frecfzen2  10155  uzennn  10164  seqeq1  10176  seq3m1  10196  monoord2  10205  ser3mono  10206  ser0f  10243  exp3vallem  10249  expm1t  10276  expeq0  10279  expubnd  10305  binom3  10364  facndiv  10440  facavg  10447  bcn0  10456  bcnp1n  10460  bcm1k  10461  bcp1nk  10463  bcval5  10464  bcn2  10465  bcp1m1  10466  bcpasc  10467  bcn2m1  10470  hashsng  10499  hashun  10506  hashfz  10522  hashfzo  10523  seq3coll  10540  shftfval  10548  2shfti  10558  resqrexlemf1  10735  abs00ap  10789  sqabs  10809  ltabs  10814  caubnd2  10844  max0addsup  10946  rexico  10948  mulcn2  11036  climaddc1  11053  climmulc2  11055  climsubc1  11056  climsubc2  11057  iserex  11063  climlec2  11065  iser3shft  11070  climcvg1nlem  11073  serf0  11076  sumrbdc  11102  fsumm1  11140  fsump1  11144  fsum00  11186  telfsumo  11190  fsumparts  11194  hashiun  11202  binomlem  11207  binom1dif  11211  bcxmas  11213  isumsplit  11215  isum1p  11216  arisum  11222  arisum2  11223  trireciplem  11224  explecnv  11229  geolim  11235  georeclim  11237  mertenslem2  11260  mertensabs  11261  efcllemp  11278  ef0lem  11280  efgt0  11304  eftlub  11310  efsep  11311  effsumlt  11312  tanval3ap  11335  efi4p  11338  resin4p  11339  recos4p  11340  ef01bndlem  11377  sin01bnd  11378  cos01bnd  11379  sin01gt0  11382  cos01gt0  11383  absefib  11391  efieq1re  11392  eirraplem  11395  dvdsdc  11413  dvdscmulr  11434  dvdslelemd  11453  odd2np1lem  11481  odd2np1  11482  flodddiv4  11543  gcdsupex  11558  gcdsupcl  11559  gcd1  11587  nn0seqcvgd  11634  algcvg  11641  algcvgblem  11642  eucalg  11652  prmind2  11713  qden1elz  11794  dfphi2  11807  phiprm  11810  phimullem  11812  oddennn  11816  xpct  11820  ennnfonelemj0  11825  ennnfonelemen  11845  ctinfomlemom  11851  restid  12042  restuni2  12257  cnrest2r  12317  lmfss  12324  lmres  12328  lmtopcnp  12330  ispsmet  12403  isxmet2d  12428  ismet2  12434  blfvalps  12465  blex  12467  xblss2  12485  reopnap  12618  divcnap  12635  climcncf  12651  cncfmpt2fcntop  12665  limcdifap  12711  cnplimcim  12716  cnlimcim  12720  cnlimc  12721  cnlimci  12722  dvbss  12734  dvcnp2cntop  12743  dvcn  12744  dvaddxxbr  12745  dvmulxxbr  12746  dvexp  12755  dveflem  12766  sinperlem  12800  sin2kpi  12803  cos2kpi  12804  sin2pim  12805  cos2pim  12806  cosq14gt0  12824  coseq0q4123  12826  pwle2  13089  nninfsellemdc  13102  sbthom  13117
  Copyright terms: Public domain W3C validator