Metamath Proof Explorer


Theorem ifpnorcor

Description: Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020)

Ref Expression
Assertion ifpnorcor if- φ ¬ φ ¬ ψ if- ψ ¬ ψ ¬ φ

Proof

Step Hyp Ref Expression
1 ifporcor if- φ φ ψ if- ψ ψ φ
2 1 notbii ¬ if- φ φ ψ ¬ if- ψ ψ φ
3 ifpnot23 ¬ if- φ φ ψ if- φ ¬ φ ¬ ψ
4 ifpnot23 ¬ if- ψ ψ φ if- ψ ¬ ψ ¬ φ
5 2 3 4 3bitr3i if- φ ¬ φ ¬ ψ if- ψ ¬ ψ ¬ φ