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  5552  dff1o2  5577  resdif  5594  f1o00  5608  ressnop0  5820  fsnunfv  5840  ovid  6121  ovidig  6122  f1stres  6305  f2ndres  6306  rdgon  6532  elixpsn  6882  diffisn  7055  diffifi  7056  unsnfi  7081  snexxph  7117  ordiso2  7202  omp1eomlem  7261  ltexnqq  7595  enq0sym  7619  prarloclem5  7687  nqprloc  7732  nqprl  7738  nqpru  7739  pitonn  8035  axcnre  8068  peano5nnnn  8079  axcaucvglemres  8086  le2tri3i  8255  muldivdirap  8854  peano5nni  9113  0nn0  9384  uzind4  9783  elfz4  10214  eluzfz  10216  ssfzo12bi  10431  ioom  10480  ser0  10755  exp3vallem  10762  hashinfuni  10999  hashxp  11048  wrdsymb1  11108  ccatfv0  11138  lswccats1fst  11175  ccatswrd  11202  ccatpfx  11233  nn0abscl  11596  fimaxre2  11738  iserle  11853  climserle  11856  summodclem2a  11892  fsumcl2lem  11909  fsumadd  11917  sumsnf  11920  isumclim3  11934  isumadd  11942  sumsplitdc  11943  fsummulc2  11959  cvgcmpub  11987  isumshft  12001  isumlessdc  12007  trireciplem  12011  geolim  12022  geo2lim  12027  cvgratz  12043  mertenslem2  12047  mertensabs  12048  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodmul  12102  prodsnf  12103  ef0lem  12171  efcvgfsum  12178  ege2le3  12182  efcj  12184  efgt1p2  12206  ndvdsadd  12442  gcdsupex  12478  gcdsupcl  12479  ialgrlemconst  12565  divgcdcoprmex  12624  1idssfct  12637  odzdvds  12768  nninfdclemp1  13021  divsfval  13361  xpsfrnel2  13379  xpsff1o  13382  mulgnndir  13688  rmodislmodlem  14314  rmodislmod  14315  tgcl  14738  txcnp  14945  ivthdich  15327  plyval  15406  lgsval2lem  15689  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsmodeq  15724  lgsmulsqcoprm  15725  2lgs  15783  bj-charfunbi  16174  bj-sucexg  16285  bj-indind  16295  bj-2inf  16301  findset  16308  trilpolemisumle  16406  nconstwlpolem0  16431