Theorem biimpri 133

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 132	. 2 |- ( ps <-> ph )
3	2	biimpi 120	1 |- ( ps -> ph )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylibr  134  sylbir  135  sylbbr  136  sylbb1  137  sylbb2  138  mpbir  146  biimtrrid  153  imbitrrdi  162  bitri  184  sylanbr  285  sylan2br  288  simplbi2  385  sylanblrc  416  mtbi  672  pm3.44  717  orbi2i  764  pm2.31  770  dcor  938  rnlem  979  syl3an1br  1289  syl3an2br  1290  syl3an3br  1291  xorbin  1404  3impexpbicom  1458  equveli  1782  sbbii  1788  dveeq2or  1839  exmoeudc  2117  nfabdw  2367  eueq2dc  2946  ralun  3355  undif3ss  3434  ssunieq  3883  a9evsep  4166  dcextest  4629  tfi  4630  peano5  4646  opelxpi  4707  ndmima  5059  iotass  5249  dffo2  5502  dff1o2  5527  resdif  5544  f1o00  5557  ressnop0  5765  fsnunfv  5785  ovid  6062  ovidig  6063  f1stres  6245  f2ndres  6246  rdgon  6472  elixpsn  6822  diffisn  6990  diffifi  6991  unsnfi  7016  snexxph  7052  ordiso2  7137  omp1eomlem  7196  ltexnqq  7521  enq0sym  7545  prarloclem5  7613  nqprloc  7658  nqprl  7664  nqpru  7665  pitonn  7961  axcnre  7994  peano5nnnn  8005  axcaucvglemres  8012  le2tri3i  8181  muldivdirap  8780  peano5nni  9039  0nn0  9310  uzind4  9709  elfz4  10140  eluzfz  10142  ssfzo12bi  10354  ioom  10403  ser0  10678  exp3vallem  10685  hashinfuni  10922  hashxp  10971  wrdsymb1  11030  ccatfv0  11059  lswccats1fst  11096  ccatswrd  11123  nn0abscl  11396  fimaxre2  11538  iserle  11653  climserle  11656  summodclem2a  11692  fsumcl2lem  11709  fsumadd  11717  sumsnf  11720  isumclim3  11734  isumadd  11742  sumsplitdc  11743  fsummulc2  11759  cvgcmpub  11787  isumshft  11801  isumlessdc  11807  trireciplem  11811  geolim  11822  geo2lim  11827  cvgratz  11843  mertenslem2  11847  mertensabs  11848  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodmul  11902  prodsnf  11903  ef0lem  11971  efcvgfsum  11978  ege2le3  11982  efcj  11984  efgt1p2  12006  ndvdsadd  12242  gcdsupex  12278  gcdsupcl  12279  ialgrlemconst  12365  divgcdcoprmex  12424  1idssfct  12437  odzdvds  12568  nninfdclemp1  12821  divsfval  13160  xpsfrnel2  13178  xpsff1o  13181  mulgnndir  13487  rmodislmodlem  14112  rmodislmod  14113  tgcl  14536  txcnp  14743  ivthdich  15125  plyval  15204  lgsval2lem  15487  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsmodeq  15522  lgsmulsqcoprm  15523  2lgs  15581  bj-charfunbi  15751  bj-sucexg  15862  bj-indind  15872  bj-2inf  15878  findset  15885  trilpolemisumle  15981  nconstwlpolem0  16006