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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 916 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 265 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
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:  simpll2  955  simprl2  961  simp1l2  1009  simp2l2  1015  simp3l2  1021  3anandirs  1254  rspc3ev  2688  tfisi  4337  brcogw  4531  oawordi  6079  nnmord  6120  nnmword  6121  ac6sfi  6382  ordiso2  6414  prarloclemarch2  6574  enq0tr  6589  distrlem4prl  6739  distrlem4pru  6740  ltaprg  6774  aptiprlemu  6795  lelttr  7164  ltletr  7165  readdcan  7213  addcan  7253  addcan2  7254  ltadd2  7487  ltmul1a  7655  ltmul1  7656  lemul1a  7898  xrlelttr  8822  xrltletr  8823  ixxdisj  8872  icoshftf1o  8959  icodisj  8960  lincmb01cmp  8971  iccf1o  8972  fztri3or  9004  modqmuladdim  9311  modqmuladdnn0  9312  q2submod  9329  modqaddmulmod  9335  ltexp2a  9466  exple1  9470  expnbnd  9533  expnlbnd2  9535  addcn2  10054  mulcn2  10056  dvdsval2  10103  dvdsadd2b  10146  dvdsmod  10166  oexpneg  10180
  Copyright terms: Public domain W3C validator