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  7494  enq0sym  7518  prarloclem5  7586  nqprloc  7631  nqprl  7637  nqpru  7638  pitonn  7934  axcnre  7967  peano5nnnn  7978  axcaucvglemres  7985  le2tri3i  8154  muldivdirap  8753  peano5nni  9012  0nn0  9283  uzind4  9681  elfz4  10112  eluzfz  10114  ssfzo12bi  10320  ioom  10369  ser0  10644  exp3vallem  10651  hashinfuni  10888  hashxp  10937  wrdsymb1  10990  nn0abscl  11269  fimaxre2  11411  iserle  11526  climserle  11529  summodclem2a  11565  fsumcl2lem  11582  fsumadd  11590  sumsnf  11593  isumclim3  11607  isumadd  11615  sumsplitdc  11616  fsummulc2  11632  cvgcmpub  11660  isumshft  11674  isumlessdc  11680  trireciplem  11684  geolim  11695  geo2lim  11700  cvgratz  11716  mertenslem2  11720  mertensabs  11721  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodmul  11775  prodsnf  11776  ef0lem  11844  efcvgfsum  11851  ege2le3  11855  efcj  11857  efgt1p2  11879  ndvdsadd  12115  gcdsupex  12151  gcdsupcl  12152  ialgrlemconst  12238  divgcdcoprmex  12297  1idssfct  12310  odzdvds  12441  nninfdclemp1  12694  divsfval  13032  xpsfrnel2  13050  xpsff1o  13053  mulgnndir  13359  rmodislmodlem  13984  rmodislmod  13985  tgcl  14408  txcnp  14615  ivthdich  14997  plyval  15076  lgsval2lem  15359  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  lgsmodeq  15394  lgsmulsqcoprm  15395  2lgs  15453  bj-charfunbi  15565  bj-sucexg  15676  bj-indind  15686  bj-2inf  15692  findset  15699  trilpolemisumle  15795  nconstwlpolem0  15820