Metamath Proof Explorer


Theorem biimt

Description: A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996)

Ref Expression
Assertion biimt φψφψ

Proof

Step Hyp Ref Expression
1 ax-1 ψφψ
2 pm2.27 φφψψ
3 1 2 impbid2 φψφψ