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  385  orc  686  pwundifss  4177  ssdomg  6640  negiso  8681  infrenegsupex  9357  xrnegiso  10999  infxrnegsupex  11000  cos01bnd  11392  cos1bnd  11393  cos2bnd  11394  sin4lt0  11400  egt2lt3  11413  epos  11414  ene1  11418  eap1  11419  slotslfn  11912  strslfvd  11927  strslfv2d  11928  strsl0  11934  setsslid  11936  setsslnid  11937  pigt2lt4  12792  pire  12794  pipos  12796  sinhalfpi  12804  tan4thpi  12849  sincos3rdpi  12851  pigt3  12852
  Copyright terms: Public domain W3C validator