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  666  nbn2  697  pm4.72  827  con4biddc  857  con1biimdc  873  bijadc  882  pclem6  1374  exbir  1436  simplbi2comg  1443  albi  1468  exbi  1604  equsexd  1729  cbv2h  1748  cbv2w  1750  sbiedh  1787  ceqsalt  2763  spcegft  2816  elab3gf  2887  euind  2924  reu6  2926  reuind  2942  sbciegft  2993  iota4  5196  fv3  5538  algcvgblem  12043  bj-inf2vnlem1  14604