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 
|- ( ph -> ( ps <-> ( ph -> ps ) ) )

Proof

Step Hyp Ref Expression
1 ax-1 
 |-  ( ps -> ( ph -> ps ) )
2 pm2.27 
 |-  ( ph -> ( ( ph -> ps ) -> ps ) )
3 1 2 impbid2 
 |-  ( ph -> ( ps <-> ( ph -> ps ) ) )