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

Theorem simpl1 967
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 964 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
21adantr 272 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
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:  simpll1  1003  simprl1  1009  simp1l1  1057  simp2l1  1063  simp3l1  1069  3anandirs  1309  rspc3ev  2778  brcogw  4676  cocan1  5654  oawordi  6331  nnmord  6379  nnmword  6380  dif1en  6739  ac6sfi  6758  ordiso2  6886  difinfsn  6951  ctssdc  6964  enq0tr  7206  distrlem4prl  7356  distrlem4pru  7357  ltaprg  7391  aptiprlemu  7412  lelttr  7816  readdcan  7866  addcan  7906  addcan2  7907  ltadd2  8145  ltmul1a  8316  ltmul1  8317  divmulassap  8415  divmulasscomap  8416  lemul1a  8573  xrlelttr  9529  xleadd1a  9596  xlesubadd  9606  icoshftf1o  9714  lincmb01cmp  9726  iccf1o  9727  fztri3or  9759  fzofzim  9905  ioom  9978  modqmuladdim  10080  modqm1p1mod0  10088  q2submod  10098  modqaddmulmod  10104  ltexp2a  10285  exple1  10289  expnlbnd2  10357  expcan  10403  fiprsshashgt1  10503  fimaxq  10513  maxleastb  10926  maxltsup  10930  xrltmaxsup  10966  xrmaxltsup  10967  xrmaxaddlem  10969  addcn2  11019  mulcn2  11021  dvdsadd2b  11436  dvdsmod  11456  oexpneg  11470  divalglemex  11515  divalg  11517  gcdass  11599  rplpwr  11611  rppwr  11612  coprmdvds2  11670  rpmulgcd2  11672  qredeq  11673  rpdvds  11676  cncongr2  11681  rpexp  11727  znege1  11751  hashgcdlem  11798  ctinf  11838  neiint  12209  topssnei  12226  iscnp4  12282  cnptopco  12286  cnconst2  12297  cnrest2  12300  cnptoprest  12303  cnpdis  12306  bldisj  12465  blgt0  12466  bl2in  12467  blss2ps  12470  blss2  12471  xblm  12481  blssps  12491  blss  12492  xmetresbl  12504  bdbl  12567  metcnp3  12575  metcnp2  12577  cncfmptc  12646  dvcnp2cntop  12706  dvcn  12707
  Copyright terms: Public domain W3C validator