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  1808  sbbii  1814  dveeq2or  1865  exmoeudc  2144  nfabdw  2403  eueq2dc  2990  ralun  3401  undif3ss  3482  ssunieq  3947  a9evsep  4232  dcextest  4703  tfi  4704  peano5  4720  opelxpi  4781  ndmima  5139  iotass  5330  dffo2  5594  dff1o2  5619  resdif  5636  f1o00  5651  ressnop0  5865  fsnunfv  5885  ovid  6170  ovidig  6171  f1stres  6353  f2ndres  6354  rdgon  6617  elixpsn  6970  modom  7061  diffisn  7150  diffifi  7151  unsnfi  7179  snexxph  7220  ordiso2  7326  omp1eomlem  7385  ltexnqq  7723  enq0sym  7747  prarloclem5  7815  nqprloc  7860  nqprl  7866  nqpru  7867  pitonn  8163  axcnre  8196  peano5nnnn  8207  axcaucvglemres  8214  le2tri3i  8382  muldivdirap  8981  peano5nni  9240  0nn0  9511  uzind4  9920  elfz4  10352  eluzfz  10354  ssfzo12bi  10570  ioom  10620  ser0  10895  exp3vallem  10902  hashinfuni  11140  hashxp  11191  wrdsymb1  11261  ccatfv0  11291  lswccats1fst  11332  ccatswrd  11362  ccatpfx  11393  nn0abscl  11770  fimaxre2  11912  iserle  12027  climserle  12030  summodclem2a  12067  fsumcl2lem  12084  fsumadd  12092  sumsnf  12095  isumclim3  12109  isumadd  12117  sumsplitdc  12118  fsummulc2  12134  cvgcmpub  12162  isumshft  12176  isumlessdc  12182  trireciplem  12186  geolim  12197  geo2lim  12202  cvgratz  12218  mertenslem2  12222  mertensabs  12223  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodmul  12277  prodsnf  12278  ef0lem  12346  efcvgfsum  12353  ege2le3  12357  efcj  12359  efgt1p2  12381  ndvdsadd  12617  gcdsupex  12653  gcdsupcl  12654  ialgrlemconst  12740  divgcdcoprmex  12799  1idssfct  12812  odzdvds  12943  nninfdclemp1  13201  divsfval  13541  xpsfrnel2  13559  xpsff1o  13562  mulgnndir  13868  rmodislmodlem  14498  rmodislmod  14499  tgcl  14929  txcnp  15136  ivthdich  15518  plyval  15597  lgsval2lem  15883  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgsmodeq  15918  lgsmulsqcoprm  15919  2lgs  15977  bj-charfunbi  16581  bj-sucexg  16692  bj-indind  16702  bj-2inf  16708  findset  16715  trilpolemisumle  16822  nconstwlpolem0  16849