Metamath Proof Explorer


Theorem trunorfalOLD

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

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

Proof

Step Hyp Ref Expression
1 df-nor
 |-  ( ( T. -\/ F. ) <-> -. ( T. \/ F. ) )
2 tru
 |-  T.
3 2 orci
 |-  ( T. \/ F. )
4 3 notnoti
 |-  -. -. ( T. \/ F. )
5 4 bifal
 |-  ( -. ( T. \/ F. ) <-> F. )
6 1 5 bitri
 |-  ( ( T. -\/ F. ) <-> F. )