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

Metamath Proof Explorer

Theorem pm2.61i

Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994) (Proof shortened by Wolf Lammen, 19-Nov-2023)

Ref Expression
Hypotheses pm2.61i.1 ⊢ ( 𝜑 → 𝜓 )
pm2.61i.2 ⊢ ( ¬ 𝜑 → 𝜓 )
Assertion pm2.61i 𝜓

Proof

Step Hyp Ref Expression
1 pm2.61i.1 ⊢ ( 𝜑 → 𝜓 )
2 pm2.61i.2 ⊢ ( ¬ 𝜑 → 𝜓 )
3 1 2 nsyl4 ⊢ ( ¬ 𝜓 → 𝜓 )
4 3 pm2.18i ⊢ 𝜓