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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117

This theorem is used by:  bicom1  131  pm5.74  179  bi3ant  224  pm5.32d  454  notbi  676  nbn2  709  pm4.72  839  con4biddc  869  con1biimdc  885  bijadc  894  pclem6  1423  exbir  1486  simplbi2comg  1493  albi  1521  exbi  1657  equsexd  1782  cbv2h  1801  cbv2w  1803  sbiedh  1840  ceqsalt  2848  spcegft  2904  elab3gf  2976  euind  3013  reu6  3015  reuind  3031  sbciegft  3082  iota4  5357  fv3  5718  algcvgblem  12827  bj-inf2vnlem1  16996