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

Theorem simpl1 918
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 915 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
21adantr 265 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ 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:  simpll1  954  simprl1  960  simp1l1  1008  simp2l1  1014  simp3l1  1020  3anandirs  1254  rspc3ev  2689  brcogw  4532  cocan1  5455  oawordi  6080  nnmord  6121  nnmword  6122  dif1en  6368  ac6sfi  6383  ordiso2  6415  enq0tr  6590  distrlem4prl  6740  distrlem4pru  6741  ltaprg  6775  aptiprlemu  6796  lelttr  7165  readdcan  7214  addcan  7254  addcan2  7255  ltadd2  7488  ltmul1a  7656  ltmul1  7657  lemul1a  7899  xrlelttr  8823  icoshftf1o  8960  lincmb01cmp  8972  iccf1o  8973  fztri3or  9005  fzofzim  9146  ioom  9217  modqmuladdim  9317  modqm1p1mod0  9325  q2submod  9335  modqaddmulmod  9341  ltexp2a  9472  exple1  9476  expnlbnd2  9542  addcn2  10062  mulcn2  10064  dvdsadd2b  10154  dvdsmod  10174  oexpneg  10188  divalglemex  10234  divalg  10236
  Copyright terms: Public domain W3C validator