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 ⊢ ¬ φ
pm3.2ni.2 ⊢ ¬ ψ
Assertion pm3.2ni ⊢ ¬ φ ∨ ψ

Proof

Step Hyp Ref Expression
1 pm3.2ni.1 ⊢ ¬ φ
2 pm3.2ni.2 ⊢ ¬ ψ
3 id ⊢ φ → φ
4 2 pm2.21i ⊢ ψ → φ
5 3 4 jaoi ⊢ φ ∨ ψ → φ
6 1 5 mto ⊢ ¬ φ ∨ ψ