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  925  rnlem  966  syl3an1br  1267  syl3an2br  1268  syl3an3br  1269  xorbin  1374  3impexpbicom  1426  equveli  1747  sbbii  1753  dveeq2or  1804  exmoeudc  2077  nfabdw  2326  eueq2dc  2898  ralun  3303  undif3ss  3382  ssunieq  3821  a9evsep  4103  dcextest  4557  tfi  4558  peano5  4574  opelxpi  4635  ndmima  4980  iotass  5169  dffo2  5413  dff1o2  5436  resdif  5453  f1o00  5466  ressnop0  5665  fsnunfv  5685  ovid  5954  ovidig  5955  f1stres  6124  f2ndres  6125  rdgon  6350  elixpsn  6697  diffisn  6855  diffifi  6856  unsnfi  6880  snexxph  6911  ordiso2  6996  omp1eomlem  7055  ltexnqq  7345  enq0sym  7369  prarloclem5  7437  nqprloc  7482  nqprl  7488  nqpru  7489  pitonn  7785  axcnre  7818  peano5nnnn  7829  axcaucvglemres  7836  le2tri3i  8003  muldivdirap  8599  peano5nni  8856  0nn0  9125  uzind4  9522  elfz4  9949  eluzfz  9951  ssfzo12bi  10156  ioom  10192  ser0  10445  exp3vallem  10452  hashinfuni  10686  hashxp  10735  nn0abscl  11023  fimaxre2  11164  iserle  11279  climserle  11282  summodclem2a  11318  fsumcl2lem  11335  fsumadd  11343  sumsnf  11346  isumclim3  11360  isumadd  11368  sumsplitdc  11369  fsummulc2  11385  cvgcmpub  11413  isumshft  11427  isumlessdc  11433  trireciplem  11437  geolim  11448  geo2lim  11453  cvgratz  11469  mertenslem2  11473  mertensabs  11474  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodmul  11528  prodsnf  11529  ef0lem  11597  efcvgfsum  11604  ege2le3  11608  efcj  11610  efgt1p2  11632  ndvdsadd  11864  gcdsupex  11886  gcdsupcl  11887  ialgrlemconst  11971  divgcdcoprmex  12030  1idssfct  12043  odzdvds  12173  nninfdclemp1  12379  tgcl  12664  txcnp  12871  lgsval2lem  13511  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsmodeq  13546  lgsmulsqcoprm  13547  bj-charfunbi  13653  bj-sucexg  13764  bj-indind  13774  bj-2inf  13780  findset  13787  trilpolemisumle  13877  nconstwlpolem0  13901