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  1459  equveli  1783  sbbii  1789  dveeq2or  1840  exmoeudc  2119  nfabdw  2369  eueq2dc  2953  ralun  3363  undif3ss  3442  ssunieq  3897  a9evsep  4182  dcextest  4647  tfi  4648  peano5  4664  opelxpi  4725  ndmima  5078  iotass  5268  dffo2  5524  dff1o2  5549  resdif  5566  f1o00  5580  ressnop0  5788  fsnunfv  5808  ovid  6085  ovidig  6086  f1stres  6268  f2ndres  6269  rdgon  6495  elixpsn  6845  diffisn  7016  diffifi  7017  unsnfi  7042  snexxph  7078  ordiso2  7163  omp1eomlem  7222  ltexnqq  7556  enq0sym  7580  prarloclem5  7648  nqprloc  7693  nqprl  7699  nqpru  7700  pitonn  7996  axcnre  8029  peano5nnnn  8040  axcaucvglemres  8047  le2tri3i  8216  muldivdirap  8815  peano5nni  9074  0nn0  9345  uzind4  9744  elfz4  10175  eluzfz  10177  ssfzo12bi  10391  ioom  10440  ser0  10715  exp3vallem  10722  hashinfuni  10959  hashxp  11008  wrdsymb1  11067  ccatfv0  11097  lswccats1fst  11134  ccatswrd  11161  ccatpfx  11192  nn0abscl  11511  fimaxre2  11653  iserle  11768  climserle  11771  summodclem2a  11807  fsumcl2lem  11824  fsumadd  11832  sumsnf  11835  isumclim3  11849  isumadd  11857  sumsplitdc  11858  fsummulc2  11874  cvgcmpub  11902  isumshft  11916  isumlessdc  11922  trireciplem  11926  geolim  11937  geo2lim  11942  cvgratz  11958  mertenslem2  11962  mertensabs  11963  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodmul  12017  prodsnf  12018  ef0lem  12086  efcvgfsum  12093  ege2le3  12097  efcj  12099  efgt1p2  12121  ndvdsadd  12357  gcdsupex  12393  gcdsupcl  12394  ialgrlemconst  12480  divgcdcoprmex  12539  1idssfct  12552  odzdvds  12683  nninfdclemp1  12936  divsfval  13275  xpsfrnel2  13293  xpsff1o  13296  mulgnndir  13602  rmodislmodlem  14227  rmodislmod  14228  tgcl  14651  txcnp  14858  ivthdich  15240  plyval  15319  lgsval2lem  15602  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsmodeq  15637  lgsmulsqcoprm  15638  2lgs  15696  bj-charfunbi  15946  bj-sucexg  16057  bj-indind  16067  bj-2inf  16073  findset  16080  trilpolemisumle  16179  nconstwlpolem0  16204