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  1770  sbbii  1776  dveeq2or  1827  exmoeudc  2105  nfabdw  2355  eueq2dc  2934  ralun  3342  undif3ss  3421  ssunieq  3869  a9evsep  4152  dcextest  4614  tfi  4615  peano5  4631  opelxpi  4692  ndmima  5043  iotass  5233  dffo2  5481  dff1o2  5506  resdif  5523  f1o00  5536  ressnop0  5740  fsnunfv  5760  ovid  6036  ovidig  6037  f1stres  6214  f2ndres  6215  rdgon  6441  elixpsn  6791  diffisn  6951  diffifi  6952  unsnfi  6977  snexxph  7011  ordiso2  7096  omp1eomlem  7155  ltexnqq  7470  enq0sym  7494  prarloclem5  7562  nqprloc  7607  nqprl  7613  nqpru  7614  pitonn  7910  axcnre  7943  peano5nnnn  7954  axcaucvglemres  7961  le2tri3i  8130  muldivdirap  8728  peano5nni  8987  0nn0  9258  uzind4  9656  elfz4  10087  eluzfz  10089  ssfzo12bi  10295  ioom  10332  ser0  10607  exp3vallem  10614  hashinfuni  10851  hashxp  10900  wrdsymb1  10953  nn0abscl  11232  fimaxre2  11373  iserle  11488  climserle  11491  summodclem2a  11527  fsumcl2lem  11544  fsumadd  11552  sumsnf  11555  isumclim3  11569  isumadd  11577  sumsplitdc  11578  fsummulc2  11594  cvgcmpub  11622  isumshft  11636  isumlessdc  11642  trireciplem  11646  geolim  11657  geo2lim  11662  cvgratz  11678  mertenslem2  11682  mertensabs  11683  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodmul  11737  prodsnf  11738  ef0lem  11806  efcvgfsum  11813  ege2le3  11817  efcj  11819  efgt1p2  11841  ndvdsadd  12075  gcdsupex  12097  gcdsupcl  12098  ialgrlemconst  12184  divgcdcoprmex  12243  1idssfct  12256  odzdvds  12386  nninfdclemp1  12610  divsfval  12914  xpsfrnel2  12932  xpsff1o  12935  mulgnndir  13224  rmodislmodlem  13849  rmodislmod  13850  tgcl  14243  txcnp  14450  ivthdich  14832  plyval  14911  lgsval2lem  15167  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsmodeq  15202  lgsmulsqcoprm  15203  2lgs  15261  bj-charfunbi  15373  bj-sucexg  15484  bj-indind  15494  bj-2inf  15500  findset  15507  trilpolemisumle  15598  nconstwlpolem0  15623