Theorem nororOLD

Description: Obsolete version of noror as of 8-Dec-2023. (Contributed by Remi, 26-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nororOLD	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 ⊽ 𝜓 ) ⊽ ( 𝜑 ⊽ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		notnotb	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ¬ ¬ ( 𝜑 ∨ 𝜓 ) )
2		df-nor	⊢ ( ( 𝜑 ⊽ 𝜓 ) ↔ ¬ ( 𝜑 ∨ 𝜓 ) )
3	2	notbii	⊢ ( ¬ ( 𝜑 ⊽ 𝜓 ) ↔ ¬ ¬ ( 𝜑 ∨ 𝜓 ) )
4		nornot	⊢ ( ¬ ( 𝜑 ⊽ 𝜓 ) ↔ ( ( 𝜑 ⊽ 𝜓 ) ⊽ ( 𝜑 ⊽ 𝜓 ) ) )
5	1 3 4	3bitr2ri	⊢ ( ( ( 𝜑 ⊽ 𝜓 ) ⊽ ( 𝜑 ⊽ 𝜓 ) ) ↔ ( 𝜑 ∨ 𝜓 ) )
6	5	bicomi	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 ⊽ 𝜓 ) ⊽ ( 𝜑 ⊽ 𝜓 ) ) )