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

Metamath Proof Explorer

Theorem pm3.2ni

Description: Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995)

Ref Expression
Hypotheses pm3.2ni.1 
|- -. ph
pm3.2ni.2 
|- -. ps
Assertion pm3.2ni 
|- -. ( ph \/ ps )

Proof

Step Hyp Ref Expression
1 pm3.2ni.1 
 |-  -. ph
2 pm3.2ni.2 
 |-  -. ps
3 id 
 |-  ( ph -> ph )
4 2 pm2.21i 
 |-  ( ps -> ph )
5 3 4 jaoi 
 |-  ( ( ph \/ ps ) -> ph )
6 1 5 mto 
 |-  -. ( ph \/ ps )