Theorem bi2 129

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		df-bi 116	. . 3 |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2	1	simpli 110	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3	2	simprd 113	1 |- ( ( ph <-> ps ) -> ( ps -> ph ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom1  130  pm5.74  178  bi3ant  223  pm5.32d  443  notbi  638  nbn2  669  pm4.72  795  con4biddc  825  con1biimdc  841  bijadc  850  pclem6  1335  exbir  1395  simplbi2comg  1402  albi  1427  exbi  1566  equsexd  1690  cbv2h  1707  sbiedh  1743  ceqsalt  2683  spcegft  2736  elab3gf  2803  euind  2840  reu6  2842  reuind  2858  sbciegft  2907  iota4  5064  fv3  5398  algcvgblem  11576  bj-inf2vnlem1  12860