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  677  pm3.44  723  orbi2i  770  pm2.31  776  dcor  944  rnlem  985  syl3an1br  1313  syl3an2br  1314  syl3an3br  1315  xorbin  1429  3impexpbicom  1484  equveli  1807  sbbii  1813  dveeq2or  1864  exmoeudc  2143  nfabdw  2394  eueq2dc  2980  ralun  3391  undif3ss  3470  ssunieq  3931  a9evsep  4216  dcextest  4685  tfi  4686  peano5  4702  opelxpi  4763  ndmima  5120  iotass  5311  dffo2  5572  dff1o2  5597  resdif  5614  f1o00  5629  ressnop0  5843  fsnunfv  5863  ovid  6148  ovidig  6149  f1stres  6331  f2ndres  6332  rdgon  6595  elixpsn  6947  modom  7037  diffisn  7125  diffifi  7126  unsnfi  7154  snexxph  7192  ordiso2  7294  omp1eomlem  7353  ltexnqq  7688  enq0sym  7712  prarloclem5  7780  nqprloc  7825  nqprl  7831  nqpru  7832  pitonn  8128  axcnre  8161  peano5nnnn  8172  axcaucvglemres  8179  le2tri3i  8347  muldivdirap  8946  peano5nni  9205  0nn0  9476  uzind4  9883  elfz4  10315  eluzfz  10317  ssfzo12bi  10533  ioom  10583  ser0  10858  exp3vallem  10865  hashinfuni  11102  hashxp  11153  wrdsymb1  11216  ccatfv0  11246  lswccats1fst  11287  ccatswrd  11317  ccatpfx  11348  nn0abscl  11725  fimaxre2  11867  iserle  11982  climserle  11985  summodclem2a  12022  fsumcl2lem  12039  fsumadd  12047  sumsnf  12050  isumclim3  12064  isumadd  12072  sumsplitdc  12073  fsummulc2  12089  cvgcmpub  12117  isumshft  12131  isumlessdc  12137  trireciplem  12141  geolim  12152  geo2lim  12157  cvgratz  12173  mertenslem2  12177  mertensabs  12178  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodmul  12232  prodsnf  12233  ef0lem  12301  efcvgfsum  12308  ege2le3  12312  efcj  12314  efgt1p2  12336  ndvdsadd  12572  gcdsupex  12608  gcdsupcl  12609  ialgrlemconst  12695  divgcdcoprmex  12754  1idssfct  12767  odzdvds  12898  nninfdclemp1  13151  divsfval  13491  xpsfrnel2  13509  xpsff1o  13512  mulgnndir  13818  rmodislmodlem  14446  rmodislmod  14447  tgcl  14875  txcnp  15082  ivthdich  15464  plyval  15543  lgsval2lem  15829  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  lgsmodeq  15864  lgsmulsqcoprm  15865  2lgs  15923  bj-charfunbi  16527  bj-sucexg  16638  bj-indind  16648  bj-2inf  16654  findset  16661  trilpolemisumle  16770  nconstwlpolem0  16796