Theorem biimpri 132

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	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
biimpri	⊢ (𝜓 → 𝜑)

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	bicomi 131	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 119	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylibr  133  sylbir  134  sylbbr  135  sylbb1  136  sylbb2  137  mpbir  145  syl5bir  152  syl6ibr  161  bitri  183  sylanbr  283  sylan2br  286  simplbi2  383  sylanblrc  413  mtbi  660  pm3.44  705  orbi2i  752  pm2.31  758  dcor  920  rnlem  961  syl3an1br  1256  syl3an2br  1257  syl3an3br  1258  xorbin  1363  3impexpbicom  1415  equveli  1733  sbbii  1739  dveeq2or  1789  exmoeudc  2063  eueq2dc  2861  ralun  3263  undif3ss  3342  ssunieq  3777  a9evsep  4058  dcextest  4503  tfi  4504  peano5  4520  opelxpi  4579  ndmima  4924  iotass  5113  dffo2  5357  dff1o2  5380  resdif  5397  f1o00  5410  ressnop0  5609  fsnunfv  5629  ovid  5895  ovidig  5896  f1stres  6065  f2ndres  6066  rdgon  6291  elixpsn  6637  diffisn  6795  diffifi  6796  unsnfi  6815  snexxph  6846  ordiso2  6928  omp1eomlem  6987  ltexnqq  7240  enq0sym  7264  prarloclem5  7332  nqprloc  7377  nqprl  7383  nqpru  7384  pitonn  7680  axcnre  7713  peano5nnnn  7724  axcaucvglemres  7731  le2tri3i  7896  muldivdirap  8491  peano5nni  8747  0nn0  9016  uzind4  9410  elfz4  9830  eluzfz  9832  ssfzo12bi  10033  ioom  10069  ser0  10318  exp3vallem  10325  hashinfuni  10555  hashxp  10604  nn0abscl  10889  fimaxre2  11030  iserle  11143  climserle  11146  summodclem2a  11182  fsumcl2lem  11199  fsumadd  11207  sumsnf  11210  isumclim3  11224  isumadd  11232  sumsplitdc  11233  fsummulc2  11249  cvgcmpub  11277  isumshft  11291  isumlessdc  11297  trireciplem  11301  geolim  11312  geo2lim  11317  cvgratz  11333  mertenslem2  11337  mertensabs  11338  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  ef0lem  11403  efcvgfsum  11410  ege2le3  11414  efcj  11416  efgt1p2  11438  ndvdsadd  11664  gcdsupex  11682  gcdsupcl  11683  ialgrlemconst  11760  divgcdcoprmex  11819  1idssfct  11832  tgcl  12272  txcnp  12479  bj-sucexg  13291  bj-indind  13301  bj-2inf  13307  findset  13314  trilpolemisumle  13406