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

Metamath Proof Explorer

Theorem pm2.65ni

Description: Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses pm2.65ni.1 ⊢ ( ¬ 𝜑 → 𝜓 )
pm2.65ni.2 ⊢ ( ¬ 𝜑 → ¬ 𝜓 )
Assertion pm2.65ni 𝜑

Proof

Step Hyp Ref Expression
1 pm2.65ni.1 ⊢ ( ¬ 𝜑 → 𝜓 )
2 pm2.65ni.2 ⊢ ( ¬ 𝜑 → ¬ 𝜓 )
3 1 2 pm2.65i ⊢ ¬ ¬ 𝜑
4 3 notnotri ⊢ 𝜑