Metamath Proof Explorer

Theorem biimp

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999)

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

Proof

Step Hyp Ref Expression
1 df-bi 
 |-  -. ( ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) -> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2 simplim 
 |-  ( -. ( ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) -> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) ) -> ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) )
3 1 2 ax-mp 
 |-  ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
4 simplim 
 |-  ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph -> ps ) )
5 3 4 syl 
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )