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  414  mtbi  665  pm3.44  710  orbi2i  757  pm2.31  763  dcor  930  rnlem  971  syl3an1br  1272  syl3an2br  1273  syl3an3br  1274  xorbin  1379  3impexpbicom  1431  equveli  1752  sbbii  1758  dveeq2or  1809  exmoeudc  2082  nfabdw  2331  eueq2dc  2903  ralun  3309  undif3ss  3388  ssunieq  3829  a9evsep  4111  dcextest  4565  tfi  4566  peano5  4582  opelxpi  4643  ndmima  4988  iotass  5177  dffo2  5424  dff1o2  5447  resdif  5464  f1o00  5477  ressnop0  5677  fsnunfv  5697  ovid  5969  ovidig  5970  f1stres  6138  f2ndres  6139  rdgon  6365  elixpsn  6713  diffisn  6871  diffifi  6872  unsnfi  6896  snexxph  6927  ordiso2  7012  omp1eomlem  7071  ltexnqq  7370  enq0sym  7394  prarloclem5  7462  nqprloc  7507  nqprl  7513  nqpru  7514  pitonn  7810  axcnre  7843  peano5nnnn  7854  axcaucvglemres  7861  le2tri3i  8028  muldivdirap  8624  peano5nni  8881  0nn0  9150  uzind4  9547  elfz4  9974  eluzfz  9976  ssfzo12bi  10181  ioom  10217  ser0  10470  exp3vallem  10477  hashinfuni  10711  hashxp  10761  nn0abscl  11049  fimaxre2  11190  iserle  11305  climserle  11308  summodclem2a  11344  fsumcl2lem  11361  fsumadd  11369  sumsnf  11372  isumclim3  11386  isumadd  11394  sumsplitdc  11395  fsummulc2  11411  cvgcmpub  11439  isumshft  11453  isumlessdc  11459  trireciplem  11463  geolim  11474  geo2lim  11479  cvgratz  11495  mertenslem2  11499  mertensabs  11500  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodmul  11554  prodsnf  11555  ef0lem  11623  efcvgfsum  11630  ege2le3  11634  efcj  11636  efgt1p2  11658  ndvdsadd  11890  gcdsupex  11912  gcdsupcl  11913  ialgrlemconst  11997  divgcdcoprmex  12056  1idssfct  12069  odzdvds  12199  nninfdclemp1  12405  tgcl  12858  txcnp  13065  lgsval2lem  13705  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsmodeq  13740  lgsmulsqcoprm  13741  bj-charfunbi  13846  bj-sucexg  13957  bj-indind  13967  bj-2inf  13973  findset  13980  trilpolemisumle  14070  nconstwlpolem0  14094