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

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

Proof of Theorem simp2
StepHypRef Expression
1 3simpa 936 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simprd 112 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simpl2  943  simpr2  946  simp2i  949  simp2d  952  simp12  970  simp22  973  simp32  976  syld3an3  1215  3ianorr  1241  stoic4b  1363  nlim0  4184  tfisi  4364  sotri2  4782  sotri3  4783  feq123  5104  sefvex  5269  fvmptt  5337  fnfvima  5467  cocan1  5504  cocan2  5505  ovexg  5616  ovmpt2x  5706  ovmpt2ga  5707  caovimo  5771  tfr1onlembxssdm  6038  tfr1onlembfn  6039  tfrcllembxssdm  6051  tfrcllembfn  6052  freccllem  6097  frecfcllem  6099  frecsuclem  6101  frecrdg  6103  mapxpen  6492  dif1en  6523  diffifi  6538  unsnfidcex  6555  unfidisj  6557  undifdc  6559  resfnfinfinss  6572  funrnfi  6574  mulcanenq  6845  ltanqg  6860  mulcanenq0ec  6905  addnnnq0  6909  distrprg  7048  aptipr  7101  addsrpr  7192  mulsrpr  7193  mulasssrg  7205  axmulass  7309  axpre-ltadd  7322  subadd2  7587  nppcan  7605  nppcan3  7607  subsub2  7611  subsub4  7616  npncan3  7621  pnpcan  7622  pnncan  7624  subcan  7638  ltadd1  7808  leadd1  7809  leadd2  7810  ltsubadd  7811  ltsubadd2  7812  lesubadd  7813  lesubadd2  7814  ltaddsub  7815  leaddsub  7817  lesub1  7835  lesub2  7836  ltsub1  7837  ltsub2  7838  gt0add  7948  apreap  7962  lemul1  7968  reapmul1lem  7969  reapmul1  7970  reapadd1  7971  remulext1  7974  remulext2  7975  apadd2  7984  mulext2  7988  mulap0r  7990  leltap  7999  ltap  8006  recexaplem2  8017  mulcanap  8030  mulcanap2  8031  divvalap  8037  divmulap  8038  divcanap1  8044  diveqap0  8045  divap0b  8046  divrecap  8051  divassap  8053  div23ap  8054  divdirap  8060  divcanap3  8061  div11ap  8063  diveqap1  8068  divmuldivap  8075  divcanap5  8077  redivclap  8094  div2negap  8098  apmul1  8151  ltdiv1  8221  ledivmul  8230  lemuldiv  8234  lt2msq1  8238  ltdiv23  8245  squeeze0  8257  zaddcllemneg  8683  eluzsub  8941  nn01to3  8995  rpgecl  9055  addlelt  9132  lbioog  9224  ubioc1  9240  ubicc2  9295  icoshftf1o  9301  fzen  9350  ubmelfzo  9498  ssfzo12  9522  ubmelm1fzo  9524  fzosplitprm1  9532  rebtwn2zlemshrink  9552  qbtwnre  9555  flqwordi  9582  flqword2  9583  flltdivnn0lt  9598  modqcl  9620  mulqmod0  9624  modqmulnn  9636  modqabs2  9652  modqmuladdnn0  9662  qnegmod  9663  addmodid  9666  modqm1p1mod0  9669  modifeq2int  9680  modqdi  9686  modqeqmodmin  9688  modfzo0difsn  9689  frec2uzf1od  9700  expnegap0  9798  expgt1  9828  exprecap  9831  expmulzap  9836  leexp2a  9843  expubnd  9847  mulbinom2  9903  bernneq2  9908  expnbnd  9910  fihashss  10057  fihashssdif  10059  shftuz  10077  shftfibg  10080  cjdivap  10168  resqrtcl  10287  absdivap  10328  abssubne0  10349  maxleast  10471  lemininf  10487  ltmininf  10488  climuni  10504  dvdsval2  10577  dvdscmulr  10603  dvdsmulcr  10604  modmulconst  10606  dvdsadd2b  10621  dvdsexp  10640  mulmoddvds  10642  divalglemeuneg  10701  gcdaddm  10753  dvdsgcdb  10780  mulgcd  10783  gcddiv  10786  lcmdvdsb  10844  mulgcddvds  10854  qredeq  10856  divgcdcoprm0  10861  cncongr1  10863  euclemma  10903  rpexp  10910  rpexp12i  10912  findset  11181
  Copyright terms: Public domain W3C validator