LLPE Home Linear Logic Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  LLPE Home  >  Th. List  >  mp Structured version  

Theorem mp 192
Description: Good ol' classic modus ponendo ponens. Doesn't it feel weird to have this be a theorem rather than an axiom?
Hypotheses
Ref Expression
mp.min 𝜑
mp.maj (𝜑𝜓)
Assertion
Ref Expression
mp 𝜓

Proof of Theorem mp
StepHypRef Expression
Colors of variables: wff var nilad
Syntax hints:  wim 180
 WARNING: This theorem has an incomplete proof.
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator