Metamath Proof Explorer

Theorem biantrurd

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995) (Proof shortened by Andrew Salmon, 7-May-2011)

Ref Expression
Hypothesis biantrud.1 φ ψ
Assertion biantrurd φ χ ψ χ


Step Hyp Ref Expression
1 biantrud.1 φ ψ
2 ibar ψ χ ψ χ
3 1 2 syl φ χ ψ χ