Theorem falnortru

Description: A -\/ identity. (Contributed by Remi, 25-Oct-2023)

	Ref	Expression
Assertion	falnortru	|- ( ( F. -\/ T. ) <-> F. )

Proof

Step	Hyp	Ref	Expression
1		norcom	|- ( ( F. -\/ T. ) <-> ( T. -\/ F. ) )
2		trunorfal	|- ( ( T. -\/ F. ) <-> F. )
3	1 2	bitri	|- ( ( F. -\/ T. ) <-> F. )