Metamath Proof Explorer


Theorem biantrur

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994)

Ref Expression
Hypothesis biantrur.1 φ
Assertion biantrur ψφψ

Proof

Step Hyp Ref Expression
1 biantrur.1 φ
2 1 biantru ψψφ
3 2 biancomi ψφψ