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

Theorem simpl2 968
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 965 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 272 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  simpll2  1004  simprl2  1010  simp1l2  1058  simp2l2  1064  simp3l2  1070  3anandirs  1309  rspc3ev  2778  tfisi  4469  brcogw  4676  oawordi  6331  nnmord  6379  nnmword  6380  ac6sfi  6758  unsnfi  6773  unsnfidcel  6775  ordiso2  6886  prarloclemarch2  7191  enq0tr  7206  distrlem4prl  7356  distrlem4pru  7357  ltaprg  7391  aptiprlemu  7412  lelttr  7816  ltletr  7817  readdcan  7866  addcan  7906  addcan2  7907  ltadd2  8145  ltmul1a  8316  ltmul1  8317  divmulassap  8415  divmulasscomap  8416  lemul1a  8573  xrlelttr  9529  xrltletr  9530  xaddass  9592  xleadd1a  9596  xltadd1  9599  xlesubadd  9606  ixxdisj  9626  icoshftf1o  9714  icodisj  9715  lincmb01cmp  9726  iccf1o  9727  fztri3or  9759  ioom  9978  modqmuladdim  10080  modqmuladdnn0  10081  q2submod  10098  modqaddmulmod  10104  exp3val  10235  ltexp2a  10285  exple1  10289  expnbnd  10355  expnlbnd2  10357  expcan  10403  fiprsshashgt1  10503  maxleastb  10926  maxltsup  10930  xrltmaxsup  10966  xrmaxltsup  10967  xrmaxaddlem  10969  xrmaxadd  10970  addcn2  11019  mulcn2  11021  geoisum1c  11229  dvdsval2  11392  dvdsadd2b  11436  dvdsmod  11456  oexpneg  11470  divalglemex  11515  divalg  11517  gcdass  11599  rplpwr  11611  rppwr  11612  lcmass  11662  coprmdvds2  11670  rpmulgcd2  11672  rpdvds  11676  cncongr2  11681  rpexp  11727  znege1  11751  hashgcdlem  11798  ctinf  11838  topssnei  12226  cnptopco  12286  cnconst2  12297  cnptoprest  12303  cnpdis  12306  upxp  12336  bldisj  12465  blgt0  12466  bl2in  12467  blss2ps  12470  blss2  12471  xblm  12481  blssps  12491  blss  12492  xmetresbl  12504  bdbl  12567  bdmopn  12568  metcnp3  12575  metcnp  12576  metcnp2  12577  dvfvalap  12693  dvcnp2cntop  12706  dvcn  12707
  Copyright terms: Public domain W3C validator