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  670  pm3.44  715  orbi2i  762  pm2.31  768  dcor  935  rnlem  976  syl3an1br  1277  syl3an2br  1278  syl3an3br  1279  xorbin  1384  3impexpbicom  1438  equveli  1759  sbbii  1765  dveeq2or  1816  exmoeudc  2089  nfabdw  2338  eueq2dc  2910  ralun  3317  undif3ss  3396  ssunieq  3842  a9evsep  4125  dcextest  4580  tfi  4581  peano5  4597  opelxpi  4658  ndmima  5005  iotass  5195  dffo2  5442  dff1o2  5466  resdif  5483  f1o00  5496  ressnop0  5697  fsnunfv  5717  ovid  5990  ovidig  5991  f1stres  6159  f2ndres  6160  rdgon  6386  elixpsn  6734  diffisn  6892  diffifi  6893  unsnfi  6917  snexxph  6948  ordiso2  7033  omp1eomlem  7092  ltexnqq  7406  enq0sym  7430  prarloclem5  7498  nqprloc  7543  nqprl  7549  nqpru  7550  pitonn  7846  axcnre  7879  peano5nnnn  7890  axcaucvglemres  7897  le2tri3i  8065  muldivdirap  8663  peano5nni  8921  0nn0  9190  uzind4  9587  elfz4  10017  eluzfz  10019  ssfzo12bi  10224  ioom  10260  ser0  10513  exp3vallem  10520  hashinfuni  10756  hashxp  10805  nn0abscl  11093  fimaxre2  11234  iserle  11349  climserle  11352  summodclem2a  11388  fsumcl2lem  11405  fsumadd  11413  sumsnf  11416  isumclim3  11430  isumadd  11438  sumsplitdc  11439  fsummulc2  11455  cvgcmpub  11483  isumshft  11497  isumlessdc  11503  trireciplem  11507  geolim  11518  geo2lim  11523  cvgratz  11539  mertenslem2  11543  mertensabs  11544  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  fprodmul  11598  prodsnf  11599  ef0lem  11667  efcvgfsum  11674  ege2le3  11678  efcj  11680  efgt1p2  11702  ndvdsadd  11935  gcdsupex  11957  gcdsupcl  11958  ialgrlemconst  12042  divgcdcoprmex  12101  1idssfct  12114  odzdvds  12244  nninfdclemp1  12450  xpsfrnel2  12764  xpsff1o  12767  mulgnndir  13010  tgcl  13534  txcnp  13741  lgsval2lem  14381  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgsmodeq  14416  lgsmulsqcoprm  14417  bj-charfunbi  14533  bj-sucexg  14644  bj-indind  14654  bj-2inf  14660  findset  14667  trilpolemisumle  14756  nconstwlpolem0  14780