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  1395  3impexpbicom  1449  equveli  1773  sbbii  1779  dveeq2or  1830  exmoeudc  2108  nfabdw  2358  eueq2dc  2937  ralun  3346  undif3ss  3425  ssunieq  3873  a9evsep  4156  dcextest  4618  tfi  4619  peano5  4635  opelxpi  4696  ndmima  5047  iotass  5237  dffo2  5487  dff1o2  5512  resdif  5529  f1o00  5542  ressnop0  5746  fsnunfv  5766  ovid  6043  ovidig  6044  f1stres  6226  f2ndres  6227  rdgon  6453  elixpsn  6803  diffisn  6963  diffifi  6964  unsnfi  6989  snexxph  7025  ordiso2  7110  omp1eomlem  7169  ltexnqq  7492  enq0sym  7516  prarloclem5  7584  nqprloc  7629  nqprl  7635  nqpru  7636  pitonn  7932  axcnre  7965  peano5nnnn  7976  axcaucvglemres  7983  le2tri3i  8152  muldivdirap  8751  peano5nni  9010  0nn0  9281  uzind4  9679  elfz4  10110  eluzfz  10112  ssfzo12bi  10318  ioom  10367  ser0  10642  exp3vallem  10649  hashinfuni  10886  hashxp  10935  wrdsymb1  10988  nn0abscl  11267  fimaxre2  11409  iserle  11524  climserle  11527  summodclem2a  11563  fsumcl2lem  11580  fsumadd  11588  sumsnf  11591  isumclim3  11605  isumadd  11613  sumsplitdc  11614  fsummulc2  11630  cvgcmpub  11658  isumshft  11672  isumlessdc  11678  trireciplem  11682  geolim  11693  geo2lim  11698  cvgratz  11714  mertenslem2  11718  mertensabs  11719  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodmul  11773  prodsnf  11774  ef0lem  11842  efcvgfsum  11849  ege2le3  11853  efcj  11855  efgt1p2  11877  ndvdsadd  12113  gcdsupex  12149  gcdsupcl  12150  ialgrlemconst  12236  divgcdcoprmex  12295  1idssfct  12308  odzdvds  12439  nninfdclemp1  12692  divsfval  13030  xpsfrnel2  13048  xpsff1o  13051  mulgnndir  13357  rmodislmodlem  13982  rmodislmod  13983  tgcl  14384  txcnp  14591  ivthdich  14973  plyval  15052  lgsval2lem  15335  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgsmodeq  15370  lgsmulsqcoprm  15371  2lgs  15429  bj-charfunbi  15541  bj-sucexg  15652  bj-indind  15662  bj-2inf  15668  findset  15675  trilpolemisumle  15769  nconstwlpolem0  15794