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

Assertion

Ref	Expression
biimpri	⊢ (𝜓 → 𝜑)

Proof of Theorem biimpri

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

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  671  pm3.44  716  orbi2i  763  pm2.31  769  dcor  937  rnlem  978  syl3an1br  1288  syl3an2br  1289  syl3an3br  1290  xorbin  1403  3impexpbicom  1457  equveli  1781  sbbii  1787  dveeq2or  1838  exmoeudc  2116  nfabdw  2366  eueq2dc  2945  ralun  3354  undif3ss  3433  ssunieq  3882  a9evsep  4165  dcextest  4628  tfi  4629  peano5  4645  opelxpi  4706  ndmima  5058  iotass  5248  dffo2  5501  dff1o2  5526  resdif  5543  f1o00  5556  ressnop0  5764  fsnunfv  5784  ovid  6061  ovidig  6062  f1stres  6244  f2ndres  6245  rdgon  6471  elixpsn  6821  diffisn  6989  diffifi  6990  unsnfi  7015  snexxph  7051  ordiso2  7136  omp1eomlem  7195  ltexnqq  7520  enq0sym  7544  prarloclem5  7612  nqprloc  7657  nqprl  7663  nqpru  7664  pitonn  7960  axcnre  7993  peano5nnnn  8004  axcaucvglemres  8011  le2tri3i  8180  muldivdirap  8779  peano5nni  9038  0nn0  9309  uzind4  9708  elfz4  10139  eluzfz  10141  ssfzo12bi  10352  ioom  10401  ser0  10676  exp3vallem  10683  hashinfuni  10920  hashxp  10969  wrdsymb1  11028  ccatfv0  11057  nn0abscl  11338  fimaxre2  11480  iserle  11595  climserle  11598  summodclem2a  11634  fsumcl2lem  11651  fsumadd  11659  sumsnf  11662  isumclim3  11676  isumadd  11684  sumsplitdc  11685  fsummulc2  11701  cvgcmpub  11729  isumshft  11743  isumlessdc  11749  trireciplem  11753  geolim  11764  geo2lim  11769  cvgratz  11785  mertenslem2  11789  mertensabs  11790  prodmodclem3  11828  prodmodclem2a  11829  zproddc  11832  fprodmul  11844  prodsnf  11845  ef0lem  11913  efcvgfsum  11920  ege2le3  11924  efcj  11926  efgt1p2  11948  ndvdsadd  12184  gcdsupex  12220  gcdsupcl  12221  ialgrlemconst  12307  divgcdcoprmex  12366  1idssfct  12379  odzdvds  12510  nninfdclemp1  12763  divsfval  13102  xpsfrnel2  13120  xpsff1o  13123  mulgnndir  13429  rmodislmodlem  14054  rmodislmod  14055  tgcl  14478  txcnp  14685  ivthdich  15067  plyval  15146  lgsval2lem  15429  lgsdir  15454  lgsdilem2  15455  lgsdi  15456  lgsne0  15457  lgsmodeq  15464  lgsmulsqcoprm  15465  2lgs  15523  bj-charfunbi  15680  bj-sucexg  15791  bj-indind  15801  bj-2inf  15807  findset  15814  trilpolemisumle  15910  nconstwlpolem0  15935