Metamath Proof Explorer

Theorem truconj

Description: Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019)

Ref Expression
Assertion truconj ⊢φ↔⊤∧φ

Proof

Step Hyp Ref Expression
1 truan ⊢⊤∧φ↔φ
2 1 bicomi ⊢φ↔⊤∧φ