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  965  albi  1619  exbi  1643  cbv2h  1991  equveliOLD  2062  sbiedOLD  2126  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  eumo0OLD  2313  2eu6  2393  2eu6OLD  2394  eleq2d  2537  ceqsalt  3141  vtoclgft  3166  spcgft  3195  pm13.183  3249  reu6  3297  reu3  3298  sbciegft  3367  fv3  5885  expeq0  12176  t1t0  19717  kqfvima  20099  ufileu  20288  cvmlift2lem1  28572  btwndiff  29604  nn0prpw  30068  bi33imp12  32739  bi23imp1  32744  bi123imp0  32745  eqsbc3rVD  33121  imbi12VD  33154  2uasbanhVD  33192  bj-dfbi6  33624  bj-bi3ant  33660  bj-cbv2hv  33777  bj-eumo0  33896  bj-ceqsalt0  33931  bj-ceqsalt1  33932  bj-ax9  33946  frege52aid  37268  bj-frege52a  37269