Metamath Proof Explorer

Theorem nic-stdmp

Description: Derive the standard modus ponens from nic-mp . (Contributed by Jeff Hoffman, 18-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses nic-smin ⊢ φ
nic-smaj ⊢ φ → ψ
Assertion nic-stdmp ⊢ ψ

Proof

Step Hyp Ref Expression
1 nic-smin ⊢ φ
2 nic-smaj ⊢ φ → ψ
3 nic-dfim ⊢ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ → ψ
4 3 nic-bi2 ⊢ φ → ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ ⊼ ψ ⊼ ψ
5 2 4 nic-mp ⊢ φ ⊼ ψ ⊼ ψ
6 1 5 nic-mp ⊢ ψ