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  lswccats1fst  11094  nn0abscl  11367  fimaxre2  11509  iserle  11624  climserle  11627  summodclem2a  11663  fsumcl2lem  11680  fsumadd  11688  sumsnf  11691  isumclim3  11705  isumadd  11713  sumsplitdc  11714  fsummulc2  11730  cvgcmpub  11758  isumshft  11772  isumlessdc  11778  trireciplem  11782  geolim  11793  geo2lim  11798  cvgratz  11814  mertenslem2  11818  mertensabs  11819  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodmul  11873  prodsnf  11874  ef0lem  11942  efcvgfsum  11949  ege2le3  11953  efcj  11955  efgt1p2  11977  ndvdsadd  12213  gcdsupex  12249  gcdsupcl  12250  ialgrlemconst  12336  divgcdcoprmex  12395  1idssfct  12408  odzdvds  12539  nninfdclemp1  12792  divsfval  13131  xpsfrnel2  13149  xpsff1o  13152  mulgnndir  13458  rmodislmodlem  14083  rmodislmod  14084  tgcl  14507  txcnp  14714  ivthdich  15096  plyval  15175  lgsval2lem  15458  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  lgsmodeq  15493  lgsmulsqcoprm  15494  2lgs  15552  bj-charfunbi  15709  bj-sucexg  15820  bj-indind  15830  bj-2inf  15836  findset  15843  trilpolemisumle  15939  nconstwlpolem0  15964