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

Metamath Proof Explorer

Theorem nanor

Description: Alternative denial in terms of disjunction and negation. This explains the name "alternative denial". (Contributed by BJ, 19-Oct-2022)

Ref Expression
Assertion nanor ⊢ φ ⊼ ψ ↔ ¬ φ ∨ ¬ ψ

Proof

Step Hyp Ref Expression
1 df-nan ⊢ φ ⊼ ψ ↔ ¬ φ ∧ ψ
2 ianor ⊢ ¬ φ ∧ ψ ↔ ¬ φ ∨ ¬ ψ
3 1 2 bitri ⊢ φ ⊼ ψ ↔ ¬ φ ∨ ¬ ψ