Metamath Proof Explorer


Theorem tradd

Description: Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019)

Ref Expression
Hypothesis tradd.1 ( 𝜑𝜓 )
Assertion tradd ( 𝜑 ↔ ( ⊤ ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 tradd.1 ( 𝜑𝜓 )
2 truan ( ( ⊤ ∧ 𝜓 ) ↔ 𝜓 )
3 1 2 bitr4i ( 𝜑 ↔ ( ⊤ ∧ 𝜓 ) )