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:  biimp  117  biimpr  129  dfbi2  386  orc  702  pwundifss  4247  ssdomg  6725  negiso  8831  infrenegsupex  9510  xrnegiso  11170  infxrnegsupex  11171  cos01bnd  11666  cos1bnd  11667  cos2bnd  11668  sin4lt0  11674  egt2lt3  11687  epos  11688  ene1  11692  eap1  11693  slotslfn  12286  strslfvd  12301  strslfv2d  12302  strsl0  12308  setsslid  12310  setsslnid  12311  reeff1o  13164  pigt2lt4  13175  pire  13177  pipos  13179  sinhalfpi  13187  tan4thpi  13232  sincos3rdpi  13234  pigt3  13235
  Copyright terms: Public domain W3C validator