Metamath Proof Explorer

Theorem falnorfal

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

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

Proof

Step Hyp Ref Expression
1 df-nor 
 |-  ( ( F. -\/ F. ) <-> -. ( F. \/ F. ) )
2 falorfal 
 |-  ( ( F. \/ F. ) <-> F. )
3 1 2 xchbinx 
 |-  ( ( F. -\/ F. ) <-> -. F. )
4 notfal 
 |-  ( -. F. <-> T. )
5 3 4 bitri 
 |-  ( ( F. -\/ F. ) <-> T. )