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

Theorem simpli 111
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 109 . 2  |-  ( (
ph  /\  ps )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-ia1 106
This theorem is referenced by:  biimp  118  biimpr  130  dfbi2  388  orc  712  pwundifss  4285  ssdomg  6777  negiso  8911  infrenegsupex  9593  xrnegiso  11269  infxrnegsupex  11270  cos01bnd  11765  cos1bnd  11766  cos2bnd  11767  sin4lt0  11773  egt2lt3  11786  epos  11787  ene1  11791  eap1  11792  slotslfn  12487  strslfvd  12503  strslfv2d  12504  strsl0  12510  setsslid  12512  setsslnid  12513  reeff1o  14164  pigt2lt4  14175  pire  14177  pipos  14179  sinhalfpi  14187  tan4thpi  14232  sincos3rdpi  14234  pigt3  14235  lgsdir2lem4  14402  lgsdir2lem5  14403
  Copyright terms: Public domain W3C validator