Theorem falnorfalOLD

Description: Obsolete version of falnorfal as of 17-Dec-2023. (Contributed by Remi, 25-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	falnorfalOLD	⊢ ( ( ⊥ ⊽ ⊥ ) ↔ ⊤ )

Proof

Step	Hyp	Ref	Expression
1		df-nor	⊢ ( ( ⊥ ⊽ ⊥ ) ↔ ¬ ( ⊥ ∨ ⊥ ) )
2		notfal	⊢ ( ¬ ⊥ ↔ ⊤ )
3	2	bicomi	⊢ ( ⊤ ↔ ¬ ⊥ )
4		falorfal	⊢ ( ( ⊥ ∨ ⊥ ) ↔ ⊥ )
5	4	bicomi	⊢ ( ⊥ ↔ ( ⊥ ∨ ⊥ ) )
6	3 5	xchbinx	⊢ ( ⊤ ↔ ¬ ( ⊥ ∨ ⊥ ) )
7	6	bicomi	⊢ ( ¬ ( ⊥ ∨ ⊥ ) ↔ ⊤ )
8	1 7	bitri	⊢ ( ( ⊥ ⊽ ⊥ ) ↔ ⊤ )