Theorem bi1 186

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

Assertion

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

Proof of Theorem bi1

Step	Hyp	Ref	Expression
1		df-bi 185	. . 3 |- -. ( ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) -> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2		simplim 151	. . 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 151	. 2 |- ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph -> ps ) )
5	3, 4	syl 16	1 |- ( ( ph <-> ps ) -> ( ph -> ps ) )

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

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 185

This theorem is referenced by:  biimpi  194  bicom1  199  biimpd  207  ibd  243  pm5.74  244  bi3antOLD  289  pm5.501  341  bija  355  bianir  958  albi  1610  exbi  1634  cbv2h  1978  equveliOLD  2049  sbiedOLD  2113  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  eumo0OLD  2300  2eu6  2380  2eu6OLD  2381  eleq2d  2524  ceqsalt  3101  vtoclgft  3126  spcgft  3155  pm13.183  3207  reu6  3255  reu3  3256  sbciegft  3325  fv3  5815  expeq0  12015  t1t0  19094  kqfvima  19445  ufileu  19634  cvmlift2lem1  27358  btwndiff  28225  nn0prpw  28689  bi33imp12  31549  bi23imp1  31554  bi123imp0  31555  eqsbc3rVD  31931  imbi12VD  31964  2uasbanhVD  32002  bj-dfbi6  32434  bj-bi3ant  32470  bj-cbv2hv  32587  bj-eumo0  32706  bj-ceqsalt0  32741  bj-ceqsalt1  32742  bj-ax9  32756