Metamath Proof Explorer


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
|- ( ( F. -\/ F. ) <-> T. )

Proof

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