Metamath Proof Explorer


Theorem norcom

Description: The connector -\/ is commutative. (Contributed by Remi, 25-Oct-2023) (Proof shortened by Wolf Lammen, 23-Apr-2024)

Ref Expression
Assertion norcom ( ( 𝜑 𝜓 ) ↔ ( 𝜓 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-nor ( ( 𝜑 𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
2 orcom ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )
3 1 2 xchbinx ( ( 𝜑 𝜓 ) ↔ ¬ ( 𝜓𝜑 ) )
4 df-nor ( ( 𝜓 𝜑 ) ↔ ¬ ( 𝜓𝜑 ) )
5 3 4 bitr4i ( ( 𝜑 𝜓 ) ↔ ( 𝜓 𝜑 ) )