Metamath Proof Explorer

Theorem biantrud

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994) (Proof shortened by Wolf Lammen, 23-Oct-2013)

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


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