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

Theorem simpli 110
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
simpli.1  |-  ( ph  /\ 
ps )
Assertion
Ref Expression
simpli  |-  ph

Proof of Theorem simpli
StepHypRef Expression
1 simpli.1 . 2  |-  ( ph  /\ 
ps )
2 simpl 108 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-ia1 105
This theorem is referenced by:  bi1  117  bi2  129  dfbi2  383  orc  684  pwundifss  4175  ssdomg  6638  negiso  8673  infrenegsupex  9341  xrnegiso  10982  infxrnegsupex  10983  cos01bnd  11375  cos1bnd  11376  cos2bnd  11377  sin4lt0  11383  egt2lt3  11393  epos  11394  ene1  11398  eap1  11399  slotslfn  11891  strslfvd  11906  strslfv2d  11907  strsl0  11913  setsslid  11915  setsslnid  11916
  Copyright terms: Public domain W3C validator