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

Theorem simpli 111
Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
simpli.1 (𝜑𝜓)
Assertion
Ref Expression
simpli 𝜑

Proof of Theorem simpli
StepHypRef Expression
1 simpli.1 . 2 (𝜑𝜓)
2 simpl 109 . 2 ((𝜑𝜓) → 𝜑)
31, 2ax-mp 5 1 𝜑
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  4287  ssdomg  6780  negiso  8914  infrenegsupex  9596  xrnegiso  11272  infxrnegsupex  11273  cos01bnd  11768  cos1bnd  11769  cos2bnd  11770  sin4lt0  11776  egt2lt3  11789  epos  11790  ene1  11794  eap1  11795  slotslfn  12490  strslfvd  12506  strslfv2d  12507  strsl0  12513  setsslid  12515  setsslnid  12516  reeff1o  14233  pigt2lt4  14244  pire  14246  pipos  14248  sinhalfpi  14256  tan4thpi  14301  sincos3rdpi  14303  pigt3  14304  lgsdir2lem4  14471  lgsdir2lem5  14472
  Copyright terms: Public domain W3C validator