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

Theorem simp1 939
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 936 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simpld 110 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
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
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simpl1  942  simpr1  945  simp1i  948  simp1d  951  simp11  969  simp21  972  simp31  975  syld3an3  1215  3ianorr  1241  stoic4a  1362  stoic4b  1363  rsp2e  2419  issod  4102  elirr  4312  sotri2  4772  sotri3  4773  funtpg  5001  funimaexglem  5033  feq123  5089  foco2  5370  ftpg  5399  fsnunf  5414  fcofo  5475  f1oiso2  5517  riotass  5546  ovmpt2x  5680  ovmpt2ga  5681  caovimo  5745  ofeq  5765  ofrval  5773  tfr1onlembxssdm  6012  tfrcllembxssdm  6025  frecsuclem  6075  frecrdg  6077  diffifi  6450  unsnfidcex  6464  unsnfidcel  6465  unfidisj  6466  undifdc  6468  ssfidc  6476  mulcanenq  6689  ltanqg  6704  addnnnq0  6753  distrlem4prl  6888  distrlem4pru  6889  distrprg  6892  aptipr  6945  addsrpr  7036  mulsrpr  7037  mulasssrg  7049  axmulass  7153  axpre-ltadd  7166  mul31  7358  addsubass  7437  subcan2  7452  subsub2  7455  subsub4  7460  npncan3  7465  pnpcan  7466  pnncan  7468  subcan  7482  subdi  7608  ltadd1  7652  leadd1  7653  leadd2  7654  ltsubadd  7655  lesubadd  7657  ltaddsub  7659  leaddsub  7661  lesub1  7679  lesub2  7680  ltsub1  7681  ltsub2  7682  ltaddsublt  7790  gt0add  7792  apreap  7806  lemul1  7812  reapmul1lem  7813  reapmul1  7814  reapadd1  7815  remulext1  7818  remulext2  7819  apadd2  7828  mulext2  7832  mulap0r  7834  leltap  7843  ltap  7850  recexaplem2  7861  mulcanap  7874  mulcanap2  7875  divvalap  7881  divcanap2  7887  diveqap0  7889  divrecap  7895  divrecap2  7896  divdirap  7904  divcanap3  7905  div11ap  7907  muldivdirap  7914  divcanap5  7921  redivclap  7938  div2negap  7942  apmul1  7995  ltdiv1  8065  ltmuldiv  8071  lemuldiv  8078  lt2msq1  8082  ltdiv23  8089  lediv23  8090  squeeze0  8101  gtndiv  8575  eluz2  8758  eluzsub  8781  peano2uz  8804  nn01to3  8835  divge1  8933  ledivge1le  8936  addlelt  8972  ixxssixx  9053  lbico1  9081  lbicc2  9134  icoshftf1o  9141  fzen  9190  fzrev3  9232  fzrevral2  9251  elfzo0  9320  elfzo0z  9322  fzosplitprm1  9372  qbtwnre  9395  flqwordi  9422  flqword2  9423  adddivflid  9426  flltdivnn0lt  9438  modqcl  9460  mulqmod0  9464  modqmulnn  9476  modqabs2  9492  addmodid  9506  modifeq2int  9520  modqeqmodmin  9528  iseqeq2  9577  iseqeq3  9578  expnegap0  9633  expgt1  9663  exprecap  9666  leexp2a  9678  expubnd  9682  sqdivap  9689  expnbnd  9745  bccmpl  9830  fihashss  9892  shftfibg  9909  mulreap  9952  abssubne0  10178  maxleast  10300  lemininf  10316  ltmininf  10317  climuni  10333  dvdscmulr  10432  dvdsmulcr  10433  summodnegmod  10434  modmulconst  10435  dvdsmultr2  10443  dvdsexp  10469  mulmoddvds  10471  modremain  10536  divgcdz  10570  gcdaddm  10582  dvdsgcdb  10609  gcdass  10611  mulgcd  10612  gcddiv  10615  rplpwr  10623  lcmdvdsb  10673  lcmass  10674  mulgcddvds  10683  qredeq  10685  qredeu  10686  rpmul  10687  divgcdcoprmex  10691  cncongr1  10692  rpexp  10739  rpexp12i  10741
  Copyright terms: Public domain W3C validator