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 
|- ( -. ph -> ps )
pm2.65ni.2 
|- ( -. ph -> -. ps )
Assertion pm2.65ni 
|- ph

Proof

Step Hyp Ref Expression
1 pm2.65ni.1 
 |-  ( -. ph -> ps )
2 pm2.65ni.2 
 |-  ( -. ph -> -. ps )
3 1 2 pm2.65i 
 |-  -. -. ph
4 3 notnotri 
 |-  ph