Metamath Proof Explorer

Theorem biimpr

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999) (Proof shortened by Wolf Lammen, 11-Nov-2012)

Ref Expression
Assertion biimpr 
|- ( ( ph <-> ps ) -> ( ps -> ph ) )

Proof

Step Hyp Ref Expression
1 dfbi1 
 |-  ( ( ph <-> ps ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
2 simprim 
 |-  ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ps -> ph ) )
3 1 2 sylbi 
 |-  ( ( ph <-> ps ) -> ( ps -> ph ) )