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  674  pm3.44  720  orbi2i  767  pm2.31  773  dcor  941  rnlem  982  syl3an1br  1310  syl3an2br  1311  syl3an3br  1312  xorbin  1426  3impexpbicom  1481  equveli  1805  sbbii  1811  dveeq2or  1862  exmoeudc  2141  nfabdw  2391  eueq2dc  2976  ralun  3386  undif3ss  3465  ssunieq  3921  a9evsep  4206  dcextest  4673  tfi  4674  peano5  4690  opelxpi  4751  ndmima  5105  iotass  5296  dffo2  5554  dff1o2  5579  resdif  5596  f1o00  5610  ressnop0  5824  fsnunfv  5844  ovid  6127  ovidig  6128  f1stres  6311  f2ndres  6312  rdgon  6538  elixpsn  6890  diffisn  7063  diffifi  7064  unsnfi  7092  snexxph  7128  ordiso2  7213  omp1eomlem  7272  ltexnqq  7606  enq0sym  7630  prarloclem5  7698  nqprloc  7743  nqprl  7749  nqpru  7750  pitonn  8046  axcnre  8079  peano5nnnn  8090  axcaucvglemres  8097  le2tri3i  8266  muldivdirap  8865  peano5nni  9124  0nn0  9395  uzind4  9795  elfz4  10226  eluzfz  10228  ssfzo12bi  10443  ioom  10492  ser0  10767  exp3vallem  10774  hashinfuni  11011  hashxp  11061  wrdsymb1  11121  ccatfv0  11151  lswccats1fst  11191  ccatswrd  11218  ccatpfx  11249  nn0abscl  11612  fimaxre2  11754  iserle  11869  climserle  11872  summodclem2a  11908  fsumcl2lem  11925  fsumadd  11933  sumsnf  11936  isumclim3  11950  isumadd  11958  sumsplitdc  11959  fsummulc2  11975  cvgcmpub  12003  isumshft  12017  isumlessdc  12023  trireciplem  12027  geolim  12038  geo2lim  12043  cvgratz  12059  mertenslem2  12063  mertensabs  12064  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodmul  12118  prodsnf  12119  ef0lem  12187  efcvgfsum  12194  ege2le3  12198  efcj  12200  efgt1p2  12222  ndvdsadd  12458  gcdsupex  12494  gcdsupcl  12495  ialgrlemconst  12581  divgcdcoprmex  12640  1idssfct  12653  odzdvds  12784  nninfdclemp1  13037  divsfval  13377  xpsfrnel2  13395  xpsff1o  13398  mulgnndir  13704  rmodislmodlem  14330  rmodislmod  14331  tgcl  14754  txcnp  14961  ivthdich  15343  plyval  15422  lgsval2lem  15705  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  lgsmodeq  15740  lgsmulsqcoprm  15741  2lgs  15799  bj-charfunbi  16257  bj-sucexg  16368  bj-indind  16378  bj-2inf  16384  findset  16391  trilpolemisumle  16494  nconstwlpolem0  16519