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  707  pwundifss  4270  ssdomg  6756  negiso  8871  infrenegsupex  9553  xrnegiso  11225  infxrnegsupex  11226  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  sin4lt0  11729  egt2lt3  11742  epos  11743  ene1  11747  eap1  11748  slotslfn  12442  strslfvd  12457  strslfv2d  12458  strsl0  12464  setsslid  12466  setsslnid  12467  reeff1o  13488  pigt2lt4  13499  pire  13501  pipos  13503  sinhalfpi  13511  tan4thpi  13556  sincos3rdpi  13558  pigt3  13559  lgsdir2lem4  13726  lgsdir2lem5  13727
  Copyright terms: Public domain W3C validator