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

Theorem simp2 916
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 912 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simprd 111 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
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  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl2  919  simpr2  922  simp2i  925  simp2d  928  simp12  946  simp22  949  simp32  952  syld3an3  1191  3ianorr  1215  stoic4b  1338  nlim0  4158  tfisi  4337  sotri2  4749  sotri3  4750  feq123  5065  sefvex  5223  fvmptt  5289  fnfvima  5420  cocan1  5454  cocan2  5455  ovexg  5566  ovmpt2x  5656  ovmpt2ga  5657  caovimo  5721  frecsuclem3  6020  dif1en  6367  diffifi  6381  mulcanenq  6540  ltanqg  6555  mulcanenq0ec  6600  addnnnq0  6604  distrprg  6743  aptipr  6796  addsrpr  6887  mulsrpr  6888  mulasssrg  6900  axmulass  7004  axpre-ltadd  7017  subadd2  7277  nppcan  7295  nppcan3  7297  subsub2  7301  subsub4  7306  npncan3  7311  pnpcan  7312  pnncan  7314  subcan  7328  ltadd1  7497  leadd1  7498  leadd2  7499  ltsubadd  7500  ltsubadd2  7501  lesubadd  7502  lesubadd2  7503  ltaddsub  7504  leaddsub  7506  lesub1  7524  lesub2  7525  ltsub1  7526  ltsub2  7527  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  divmulap  7727  divcanap1  7733  diveqap0  7734  divap0b  7735  divrecap  7740  divassap  7742  div23ap  7743  divdirap  7747  divcanap3  7748  div11ap  7750  diveqap1  7755  divmuldivap  7762  divcanap5  7764  redivclap  7781  div2negap  7785  apmul1  7838  ltdiv1  7908  ledivmul  7917  lemuldiv  7921  lt2msq1  7925  ltdiv23  7932  squeeze0  7944  zaddcllemneg  8340  eluzsub  8597  nn01to3  8648  rpgecl  8708  addlelt  8785  lbioog  8882  ubioc1  8898  ubicc2  8953  icoshftf1o  8959  fzen  9008  ubmelfzo  9157  ssfzo12  9181  ubmelm1fzo  9183  fzosplitprm1  9191  qbtwnzlemshrink  9205  rebtwn2zlemshrink  9209  qbtwnre  9212  flqwordi  9237  flqword2  9238  flltdivnn0lt  9253  modqcl  9275  mulqmod0  9279  modqmulnn  9291  modqabs2  9307  modqmuladdnn0  9317  qnegmod  9318  addmodid  9321  modqm1p1mod0  9324  modifeq2int  9335  modqdi  9341  modqeqmodmin  9343  modfzo0difsn  9344  frec2uzf1od  9355  expnegap0  9427  expgt1  9457  exprecap  9460  expmulzap  9465  leexp2a  9472  expubnd  9476  mulbinom2  9532  bernneq2  9537  expnbnd  9539  shftuz  9645  shftfibg  9648  cjdivap  9736  resqrtcl  9855  absdivap  9896  abssubne0  9917  climuni  10044  dvdsval2  10110  dvdscmulr  10135  dvdsmulcr  10136  modmulconst  10138  dvdsadd2b  10153  dvdsexp  10172  mulmoddvds  10174  findset  10436
  Copyright terms: Public domain W3C validator