Theorem bi2 189

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Assertion

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

Proof of Theorem bi2

Step	Hyp	Ref	Expression
1		dfbi1 184	. 2 |- ((ph <-> ps) <-> -. ((ph -> ps) -> -. (ps -> ph)))
2		simprim 142	. 2 |- (-. ((ph -> ps) -> -. (ps -> ph)) -> (ps -> ph))
3	1, 2	sylbi 187	1 |- ((ph <-> ps) -> (ps -> ph))

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:  bicom1  190  pm5.74  235  bi3ant  280  bija  344  pm4.72  846  exbir  1365  simplbi2comg  1373  albi  1564  exbi  1581  cbv2h  1980  sbied  2036  2eu6  2289  ceqsalt  2881  euind  3023  reu6  3025  reuind  3039  sbciegft  3076  iota4  4357  fv3  5341