Metamath Proof Explorer


Theorem bianir

Description: A closed form of mpbir , analogous to pm2.27 (assertion). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Roger Witte, 17-Aug-2020)

Ref Expression
Assertion bianir
|- ( ( ph /\ ( ps <-> ph ) ) -> ps )

Proof

Step Hyp Ref Expression
1 biimpr
 |-  ( ( ps <-> ph ) -> ( ph -> ps ) )
2 1 impcom
 |-  ( ( ph /\ ( ps <-> ph ) ) -> ps )