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  671  pm3.44  716  orbi2i  763  pm2.31  769  dcor  937  rnlem  978  syl3an1br  1288  syl3an2br  1289  syl3an3br  1290  xorbin  1395  3impexpbicom  1449  equveli  1770  sbbii  1776  dveeq2or  1827  exmoeudc  2105  nfabdw  2355  eueq2dc  2933  ralun  3341  undif3ss  3420  ssunieq  3868  a9evsep  4151  dcextest  4613  tfi  4614  peano5  4630  opelxpi  4691  ndmima  5042  iotass  5232  dffo2  5480  dff1o2  5505  resdif  5522  f1o00  5535  ressnop0  5739  fsnunfv  5759  ovid  6035  ovidig  6036  f1stres  6212  f2ndres  6213  rdgon  6439  elixpsn  6789  diffisn  6949  diffifi  6950  unsnfi  6975  snexxph  7009  ordiso2  7094  omp1eomlem  7153  ltexnqq  7468  enq0sym  7492  prarloclem5  7560  nqprloc  7605  nqprl  7611  nqpru  7612  pitonn  7908  axcnre  7941  peano5nnnn  7952  axcaucvglemres  7959  le2tri3i  8128  muldivdirap  8726  peano5nni  8985  0nn0  9255  uzind4  9653  elfz4  10084  eluzfz  10086  ssfzo12bi  10292  ioom  10329  ser0  10604  exp3vallem  10611  hashinfuni  10848  hashxp  10897  wrdsymb1  10950  nn0abscl  11229  fimaxre2  11370  iserle  11485  climserle  11488  summodclem2a  11524  fsumcl2lem  11541  fsumadd  11549  sumsnf  11552  isumclim3  11566  isumadd  11574  sumsplitdc  11575  fsummulc2  11591  cvgcmpub  11619  isumshft  11633  isumlessdc  11639  trireciplem  11643  geolim  11654  geo2lim  11659  cvgratz  11675  mertenslem2  11679  mertensabs  11680  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodmul  11734  prodsnf  11735  ef0lem  11803  efcvgfsum  11810  ege2le3  11814  efcj  11816  efgt1p2  11838  ndvdsadd  12072  gcdsupex  12094  gcdsupcl  12095  ialgrlemconst  12181  divgcdcoprmex  12240  1idssfct  12253  odzdvds  12383  nninfdclemp1  12607  divsfval  12911  xpsfrnel2  12929  xpsff1o  12932  mulgnndir  13221  rmodislmodlem  13846  rmodislmod  13847  tgcl  14232  txcnp  14439  ivthdich  14807  plyval  14878  lgsval2lem  15126  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgsmodeq  15161  lgsmulsqcoprm  15162  bj-charfunbi  15303  bj-sucexg  15414  bj-indind  15424  bj-2inf  15430  findset  15437  trilpolemisumle  15528  nconstwlpolem0  15553