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

Theorem simpli 110
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 108 . 2 ((𝜑𝜓) → 𝜑)
31, 2ax-mp 5 1 𝜑
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  701  pwundifss  4202  ssdomg  6665  negiso  8706  infrenegsupex  9382  xrnegiso  11024  infxrnegsupex  11025  cos01bnd  11454  cos1bnd  11455  cos2bnd  11456  sin4lt0  11462  egt2lt3  11475  epos  11476  ene1  11480  eap1  11481  slotslfn  11974  strslfvd  11989  strslfv2d  11990  strsl0  11996  setsslid  11998  setsslnid  11999  pigt2lt4  12854  pire  12856  pipos  12858  sinhalfpi  12866  tan4thpi  12911  sincos3rdpi  12913  pigt3  12914
  Copyright terms: Public domain W3C validator