Theorem biimpri 132

Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)

Hypothesis

Ref	Expression
biimpri.1	|- ( ph <-> ps )

Assertion

Ref	Expression
biimpri	|- ( ps -> ph )

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 |- ( ph <-> ps )
2	1	bicomi 131	. 2 |- ( ps <-> ph )
3	2	biimpi 119	1 |- ( ps -> ph )

Syntax hints:   -> wi 4   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylibr  133  sylbir  134  sylbbr  135  sylbb1  136  sylbb2  137  mpbir  145  syl5bir  152  syl6ibr  161  bitri  183  sylanbr  281  sylan2br  284  simplbi2  380  sylanblrc  410  mtbi  642  pm3.44  687  orbi2i  734  pm2.31  740  dcor  900  rnlem  941  syl3an1br  1236  syl3an2br  1237  syl3an3br  1238  xorbin  1343  3impexpbicom  1395  equveli  1713  sbbii  1719  dveeq2or  1768  exmoeudc  2036  eueq2dc  2824  ralun  3222  undif3ss  3301  ssunieq  3733  a9evsep  4008  dcextest  4453  tfi  4454  peano5  4470  opelxpi  4529  ndmima  4872  iotass  5061  dffo2  5305  dff1o2  5326  resdif  5343  f1o00  5356  ressnop0  5553  fsnunfv  5573  ovid  5839  ovidig  5840  f1stres  6009  f2ndres  6010  rdgon  6235  elixpsn  6581  diffisn  6738  diffifi  6739  unsnfi  6758  snexxph  6788  ordiso2  6870  omp1eomlem  6929  ltexnqq  7158  enq0sym  7182  prarloclem5  7250  nqprloc  7295  nqprl  7301  nqpru  7302  pitonn  7577  axcnre  7610  peano5nnnn  7621  axcaucvglemres  7628  le2tri3i  7789  muldivdirap  8374  peano5nni  8627  0nn0  8890  uzind4  9279  elfz4  9686  eluzfz  9688  ssfzo12bi  9889  ioom  9925  ser0  10174  exp3vallem  10181  hashinfuni  10410  hashxp  10459  nn0abscl  10743  fimaxre2  10884  iserle  10997  climserle  11000  summodclem2a  11036  fsumcl2lem  11053  fsumadd  11061  sumsnf  11064  isumclim3  11078  isumadd  11086  sumsplitdc  11087  fsummulc2  11103  cvgcmpub  11131  isumshft  11145  isumlessdc  11151  trireciplem  11155  geolim  11166  geo2lim  11171  cvgratz  11187  mertenslem2  11191  mertensabs  11192  ef0lem  11211  efcvgfsum  11218  ege2le3  11222  efcj  11224  efgt1p2  11246  ndvdsadd  11470  gcdsupex  11488  gcdsupcl  11489  ialgrlemconst  11564  divgcdcoprmex  11623  1idssfct  11636  tgcl  12070  txcnp  12276  bj-sucexg  12803  bj-indind  12813  bj-2inf  12819  findset  12826  trilpolemisumle  12912