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  4286  ssdomg  6778  negiso  8912  infrenegsupex  9594  xrnegiso  11270  infxrnegsupex  11271  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  sin4lt0  11774  egt2lt3  11787  epos  11788  ene1  11792  eap1  11793  slotslfn  12488  strslfvd  12504  strslfv2d  12505  strsl0  12511  setsslid  12513  setsslnid  12514  reeff1o  14197  pigt2lt4  14208  pire  14210  pipos  14212  sinhalfpi  14220  tan4thpi  14265  sincos3rdpi  14267  pigt3  14268  lgsdir2lem4  14435  lgsdir2lem5  14436
  Copyright terms: Public domain W3C validator