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 ( ( ⊤ ⊥ ) ↔ ⊥ )

Proof

Step Hyp Ref Expression
1 df-nor ( ( ⊤ ⊥ ) ↔ ¬ ( ⊤ ∨ ⊥ ) )
2 tru
3 2 orci ( ⊤ ∨ ⊥ )
4 3 notnoti ¬ ¬ ( ⊤ ∨ ⊥ )
5 4 bifal ( ¬ ( ⊤ ∨ ⊥ ) ↔ ⊥ )
6 1 5 bitri ( ( ⊤ ⊥ ) ↔ ⊥ )