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

Theorem simp1 915
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp1  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )

Proof of Theorem simp1
StepHypRef Expression
1 3simpa 912 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simpld 109 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl1  918  simpr1  921  simp1i  924  simp1d  927  simp11  945  simp21  948  simp31  951  syld3an3  1191  3ianorr  1215  stoic4a  1337  stoic4b  1338  rsp2e  2389  issod  4083  elirr  4293  sotri2  4749  sotri3  4750  funtpg  4977  funimaexglem  5009  feq123  5065  foco2  5345  ftpg  5374  fsnunf  5389  fcofo  5451  f1oiso2  5493  riotass  5522  ovmpt2x  5656  ovmpt2ga  5657  caovimo  5721  ofeq  5741  ofrval  5749  frecsuclem3  6020  diffifi  6381  mulcanenq  6540  ltanqg  6555  addnnnq0  6604  distrlem4prl  6739  distrlem4pru  6740  distrprg  6743  aptipr  6796  addsrpr  6887  mulsrpr  6888  mulasssrg  6900  axmulass  7004  axpre-ltadd  7017  mul31  7204  addsubass  7283  subcan2  7298  subsub2  7301  subsub4  7306  npncan3  7311  pnpcan  7312  pnncan  7314  subcan  7328  subdi  7453  ltadd1  7497  leadd1  7498  leadd2  7499  ltsubadd  7500  lesubadd  7502  ltaddsub  7504  leaddsub  7506  lesub1  7524  lesub2  7525  ltsub1  7526  ltsub2  7527  ltaddsublt  7635  gt0add  7637  apreap  7651  lemul1  7657  reapmul1lem  7658  reapmul1  7659  reapadd1  7660  remulext1  7663  remulext2  7664  apadd2  7673  mulext2  7677  mulap0r  7679  leltap  7688  ltap  7695  recexaplem2  7706  mulcanap  7719  mulcanap2  7720  divvalap  7726  divcanap2  7732  diveqap0  7734  divrecap  7740  divrecap2  7741  divdirap  7747  divcanap3  7748  div11ap  7750  muldivdirap  7757  divcanap5  7764  redivclap  7781  div2negap  7785  apmul1  7838  ltdiv1  7908  ltmuldiv  7914  lemuldiv  7921  lt2msq1  7925  ltdiv23  7932  lediv23  7933  squeeze0  7944  gtndiv  8392  eluz2  8574  eluzsub  8597  peano2uz  8621  nn01to3  8648  divge1  8746  ledivge1le  8749  addlelt  8785  ixxssixx  8871  lbico1  8899  lbicc2  8952  icoshftf1o  8959  fzen  9008  fzrev3  9050  fzrevral2  9069  elfzo0  9139  elfzo0z  9141  fzosplitprm1  9191  qbtwnre  9212  flqwordi  9232  flqword2  9233  adddivflid  9236  flltdivnn0lt  9248  modqcl  9270  mulqmod0  9274  modqmulnn  9286  modqabs2  9302  addmodid  9316  modifeq2int  9330  modqeqmodmin  9338  iseqeq2  9373  iseqeq3  9374  expnegap0  9422  expgt1  9452  exprecap  9455  leexp2a  9467  expubnd  9471  sqdivap  9478  expnbnd  9533  bccmpl  9615  shftfibg  9642  mulreap  9685  abssubne0  9910  climuni  10037  dvdscmulr  10128  dvdsmulcr  10129  summodnegmod  10130  modmulconst  10131  dvdsmultr2  10139  dvdsexp  10165  mulmoddvds  10167
  Copyright terms: Public domain W3C validator