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

Theorem simp2 942
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 938 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simprd 112 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 922
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 924
This theorem is referenced by:  simpl2  945  simpr2  948  simp2i  951  simp2d  954  simp12  972  simp22  975  simp32  978  syld3an3  1217  3ianorr  1243  stoic4b  1365  nlim0  4195  tfisi  4375  sotri2  4796  sotri3  4797  feq123  5118  sefvex  5289  fvmptt  5357  fnfvima  5490  cocan1  5527  cocan2  5528  ovexg  5640  ovmpt2x  5730  ovmpt2ga  5731  caovimo  5795  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfrcllembxssdm  6075  tfrcllembfn  6076  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecrdg  6127  mapxpen  6516  dif1en  6547  diffifi  6562  unsnfidcex  6582  unfidisj  6584  undifdc  6586  resfnfinfinss  6599  funrnfi  6601  sbthlemi9  6618  mulcanenq  6888  ltanqg  6903  mulcanenq0ec  6948  addnnnq0  6952  distrprg  7091  aptipr  7144  addsrpr  7235  mulsrpr  7236  mulasssrg  7248  axmulass  7352  axpre-ltadd  7365  subadd2  7630  nppcan  7648  nppcan3  7650  subsub2  7654  subsub4  7659  npncan3  7664  pnpcan  7665  pnncan  7667  subcan  7681  ltadd1  7851  leadd1  7852  leadd2  7853  ltsubadd  7854  ltsubadd2  7855  lesubadd  7856  lesubadd2  7857  ltaddsub  7858  leaddsub  7860  lesub1  7878  lesub2  7879  ltsub1  7880  ltsub2  7881  gt0add  7991  apreap  8005  lemul1  8011  reapmul1lem  8012  reapmul1  8013  reapadd1  8014  remulext1  8017  remulext2  8018  apadd2  8027  mulext2  8031  mulap0r  8033  leltap  8042  ltap  8049  recexaplem2  8060  mulcanap  8073  mulcanap2  8074  divvalap  8080  divmulap  8081  divcanap1  8087  diveqap0  8088  divap0b  8089  divrecap  8094  divassap  8096  div23ap  8097  divdirap  8103  divcanap3  8104  div11ap  8106  diveqap1  8111  divmuldivap  8118  divcanap5  8120  redivclap  8137  div2negap  8141  apmul1  8194  ltdiv1  8264  ledivmul  8273  lemuldiv  8277  lt2msq1  8281  ltdiv23  8288  squeeze0  8300  zaddcllemneg  8722  eluzsub  8980  nn01to3  9034  rpgecl  9094  addlelt  9171  lbioog  9263  ubioc1  9279  ubicc2  9334  icoshftf1o  9340  fzen  9389  ubmelfzo  9539  ssfzo12  9563  ubmelm1fzo  9565  fzosplitprm1  9573  rebtwn2zlemshrink  9593  qbtwnre  9596  flqwordi  9623  flqword2  9624  flltdivnn0lt  9639  modqcl  9661  mulqmod0  9665  modqmulnn  9677  modqabs2  9693  modqmuladdnn0  9703  qnegmod  9704  addmodid  9707  modqm1p1mod0  9710  modifeq2int  9721  modqdi  9727  modqeqmodmin  9729  modfzo0difsn  9730  frec2uzf1od  9741  expnegap0  9861  expgt1  9891  exprecap  9894  expmulzap  9899  leexp2a  9906  expubnd  9910  mulbinom2  9966  bernneq2  9971  expnbnd  9973  fihashss  10120  fihashssdif  10122  fimaxq  10131  shftuz  10147  shftfibg  10150  cjdivap  10238  resqrtcl  10357  absdivap  10398  abssubne0  10419  maxleast  10541  lemininf  10557  ltmininf  10558  climuni  10574  isumz  10667  dvdsval2  10674  dvdscmulr  10700  dvdsmulcr  10701  modmulconst  10703  dvdsadd2b  10718  dvdsexp  10737  mulmoddvds  10739  divalglemeuneg  10798  gcdaddm  10850  dvdsgcdb  10877  mulgcd  10880  gcddiv  10883  lcmdvdsb  10941  mulgcddvds  10951  qredeq  10953  divgcdcoprm0  10958  cncongr1  10960  euclemma  11000  rpexp  11007  rpexp12i  11009  findset  11278
  Copyright terms: Public domain W3C validator