Theorem biimpr 130

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

Assertion

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

Proof of Theorem biimpr

Step	Hyp	Ref	Expression
1		df-bi 117	. . 3 |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2	1	simpli 111	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3	2	simprd 114	1 |- ( ( ph <-> ps ) -> ( ps -> ph ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bicom1  131  pm5.74  179  bi3ant  224  pm5.32d  450  notbi  672  nbn2  704  pm4.72  834  con4biddc  864  con1biimdc  880  bijadc  889  pclem6  1418  exbir  1481  simplbi2comg  1488  albi  1516  exbi  1652  equsexd  1776  cbv2h  1795  cbv2w  1797  sbiedh  1834  ceqsalt  2828  spcegft  2884  elab3gf  2955  euind  2992  reu6  2994  reuind  3010  sbciegft  3061  iota4  5305  fv3  5662  algcvgblem  12641  bj-inf2vnlem1  16623