Metamath Proof Explorer


Theorem ifpxorcor

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

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

Proof

Step Hyp Ref Expression
1 ifpbicor if- φ ¬ ψ ¬ ¬ ψ if- ¬ ψ φ ¬ φ
2 notnotb ψ ¬ ¬ ψ
3 ifpbi3 ψ ¬ ¬ ψ if- φ ¬ ψ ψ if- φ ¬ ψ ¬ ¬ ψ
4 2 3 ax-mp if- φ ¬ ψ ψ if- φ ¬ ψ ¬ ¬ ψ
5 ifpn if- ψ ¬ φ φ if- ¬ ψ φ ¬ φ
6 1 4 5 3bitr4i if- φ ¬ ψ ψ if- ψ ¬ φ φ