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 ψ φ ψ