Metamath Proof Explorer


Theorem trunortruOLD

Description: Obsolete version of trunortru as of 7-Dec-2023. (Contributed by Remi, 25-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion trunortruOLD ( ( ⊤ ⊤ ) ↔ ⊥ )

Proof

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