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 ⊢ φ ↔ ⊤ ∧ φ