Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Truth tables
Disjunction
truorfal
Next ⟩
falortru
Metamath Proof Explorer
Ascii
Structured
Theorem
truorfal
Description:
A
\/
identity.
(Contributed by
Anthony Hart
, 22-Oct-2010)
Ref
Expression
Assertion
truorfal
⊢
( ( ⊤ ∨ ⊥ ) ↔ ⊤ )
Proof
Step
Hyp
Ref
Expression
1
tru
⊢
⊤
2
1
orci
⊢
( ⊤ ∨ ⊥ )
3
2
bitru
⊢
( ( ⊤ ∨ ⊥ ) ↔ ⊤ )