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-mp 5  ax-1 6  ax-2 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  283  sylan2br  286  simplbi2  383  sylanblrc  413  mtbi  660  pm3.44  705  orbi2i  752  pm2.31  758  dcor  920  rnlem  961  syl3an1br  1259  syl3an2br  1260  syl3an3br  1261  xorbin  1366  3impexpbicom  1418  equveli  1739  sbbii  1745  dveeq2or  1796  exmoeudc  2069  nfabdw  2318  eueq2dc  2885  ralun  3289  undif3ss  3368  ssunieq  3805  a9evsep  4086  dcextest  4538  tfi  4539  peano5  4555  opelxpi  4615  ndmima  4960  iotass  5149  dffo2  5393  dff1o2  5416  resdif  5433  f1o00  5446  ressnop0  5645  fsnunfv  5665  ovid  5931  ovidig  5932  f1stres  6101  f2ndres  6102  rdgon  6327  elixpsn  6673  diffisn  6831  diffifi  6832  unsnfi  6856  snexxph  6887  ordiso2  6969  omp1eomlem  7028  ltexnqq  7311  enq0sym  7335  prarloclem5  7403  nqprloc  7448  nqprl  7454  nqpru  7455  pitonn  7751  axcnre  7784  peano5nnnn  7795  axcaucvglemres  7802  le2tri3i  7968  muldivdirap  8563  peano5nni  8819  0nn0  9088  uzind4  9482  elfz4  9903  eluzfz  9905  ssfzo12bi  10106  ioom  10142  ser0  10395  exp3vallem  10402  hashinfuni  10633  hashxp  10682  nn0abscl  10967  fimaxre2  11108  iserle  11221  climserle  11224  summodclem2a  11260  fsumcl2lem  11277  fsumadd  11285  sumsnf  11288  isumclim3  11302  isumadd  11310  sumsplitdc  11311  fsummulc2  11327  cvgcmpub  11355  isumshft  11369  isumlessdc  11375  trireciplem  11379  geolim  11390  geo2lim  11395  cvgratz  11411  mertenslem2  11415  mertensabs  11416  prodmodclem3  11454  prodmodclem2a  11455  zproddc  11458  fprodmul  11470  prodsnf  11471  ef0lem  11539  efcvgfsum  11546  ege2le3  11550  efcj  11552  efgt1p2  11574  ndvdsadd  11803  gcdsupex  11821  gcdsupcl  11822  ialgrlemconst  11900  divgcdcoprmex  11959  1idssfct  11972  tgcl  12424  txcnp  12631  bj-charfunbi  13346  bj-sucexg  13457  bj-indind  13467  bj-2inf  13473  findset  13480  trilpolemisumle  13572  nconstwlpolem0  13596