This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm2.24i

Description: Inference associated with pm2.24 . Its associated inference is pm2.24ii . (Contributed by NM, 20-Aug-2001)

Ref Expression
Hypothesis pm2.24i.1 ⊢ 𝜑
Assertion pm2.24i ( ¬ 𝜑 → 𝜓 )

Proof

Step Hyp Ref Expression
1 pm2.24i.1 ⊢ 𝜑
2 1 a1i ⊢ ( ¬ 𝜓 → 𝜑 )
3 2 con1i ⊢ ( ¬ 𝜑 → 𝜓 )