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  967  albi  1640  exbi  1667  cbv2h  2020  equveliOLD  2090  mo2v  2290  mo2vOLD  2291  mo2vOLDOLD  2292  eumo0OLD  2318  2eu6  2383  2eu6OLD  2384  eleq2d  2527  ceqsalt  3132  vtoclgft  3157  spcgft  3186  pm13.183  3240  reu6  3288  reu3  3289  sbciegft  3358  fv3  5885  expeq0  12199  t1t0  19976  kqfvima  20357  ufileu  20546  cvmlift2lem1  28944  btwndiff  29882  nn0prpw  30346  bi33imp12  33402  bi23imp1  33407  bi123imp0  33408  eqsbc3rVD  33783  imbi12VD  33816  2uasbanhVD  33854  bj-dfbi6  34299  bj-bi3ant  34321  bj-cbv2hv  34437  bj-eumo0  34557  bj-ceqsalt0  34592  bj-ceqsalt1  34593  bj-ax9  34607