Metamath Proof Explorer


Theorem pm2.6

Description: Theorem *2.6 of WhiteheadRussell p. 107. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm2.6 ⊢ ¬ φ → ψ → φ → ψ → ψ

Proof

Step Hyp Ref Expression
1 id ⊢ ¬ φ → ψ → ¬ φ → ψ
2 idd ⊢ ¬ φ → ψ → ψ → ψ
3 1 2 jad ⊢ ¬ φ → ψ → φ → ψ → ψ