Theorem biimp 205

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

Assertion

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

Proof of Theorem biimp

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  biimpi  206  bicom1  211  biimpd  219  ibd  258  pm5.74  259  pm5.501  356  bija  370  albi  1746  cbv2h  2269  mo2v  2477  2eu6  2558  ceqsalt  3228  vtoclgft  3254  vtoclgftOLD  3255  spcgft  3285  pm13.183  3344  reu6  3395  reu3  3396  sbciegft  3466  fv3  6206  expeq0  12890  t1t0  21152  kqfvima  21533  ufileu  21723  cvmlift2lem1  31284  btwndiff  32134  nn0prpw  32318  bj-dfbi6  32560  bj-bi3ant  32574  bj-ssbbi  32622  bj-cbv2hv  32731  bj-eumo0  32830  bj-ceqsalt0  32873  bj-ceqsalt1  32874  bj-ax9  32890  bj-ax9-2  32891  or3or  38319  bi33imp12  38696  bi23imp1  38701  bi123imp0  38702  eqsbc3rVD  39075  imbi12VD  39109  2uasbanhVD  39147