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 ⊢ ⊥ ⊽ ⊥ ↔ ⊤

Proof

Step Hyp Ref Expression
1 df-nor ⊢ ⊥ ⊽ ⊥ ↔ ¬ ⊥ ∨ ⊥
2 notfal ⊢ ¬ ⊥ ↔ ⊤
3 2 bicomi ⊢ ⊤ ↔ ¬ ⊥
4 falorfal ⊢ ⊥ ∨ ⊥ ↔ ⊥
5 4 bicomi ⊢ ⊥ ↔ ⊥ ∨ ⊥
6 3 5 xchbinx ⊢ ⊤ ↔ ¬ ⊥ ∨ ⊥
7 6 bicomi ⊢ ¬ ⊥ ∨ ⊥ ↔ ⊤
8 1 7 bitri ⊢ ⊥ ⊽ ⊥ ↔ ⊤