Metamath Proof Explorer

Theorem trunortru

Description: A -\/ identity. (Contributed by Remi, 25-Oct-2023) (Proof shortened by Wolf Lammen, 7-Dec-2023)

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

Proof

Step Hyp Ref Expression
1 df-nor 
 |-  ( ( T. -\/ T. ) <-> -. ( T. \/ T. ) )
2 truortru 
 |-  ( ( T. \/ T. ) <-> T. )
3 1 2 xchbinx 
 |-  ( ( T. -\/ T. ) <-> -. T. )
4 df-fal 
 |-  ( F. <-> -. T. )
5 3 4 bitr4i 
 |-  ( ( T. -\/ T. ) <-> F. )