Theorem bi1 178

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 177	. . 3 |- -. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps)))
2		simplim 143	. . 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 143	. 2 |- (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph -> ps))
5	3, 4	syl 15	1 |- ((ph <-> ps) -> (ph -> ps))

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

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 177

This theorem is referenced by:  biimpi  186  bicom1  190  biimpd  198  ibd  234  pm5.74  235  bi3ant  280  pm5.501  330  bija  344  albi  1564  exbi  1581  cbv2h  1980  sbied  2036  eumo0  2228  2eu6  2289  ceqsalt  2882  vtoclgft  2906  spcgft  2932  pm13.183  2980  reu6  3026  reu3  3027  sbciegft  3077  fv3  5342