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  674  pm3.44  720  orbi2i  767  pm2.31  773  dcor  941  rnlem  982  syl3an1br  1310  syl3an2br  1311  syl3an3br  1312  xorbin  1426  3impexpbicom  1481  equveli  1805  sbbii  1811  dveeq2or  1862  exmoeudc  2141  nfabdw  2391  eueq2dc  2976  ralun  3386  undif3ss  3465  ssunieq  3921  a9evsep  4206  dcextest  4673  tfi  4674  peano5  4690  opelxpi  4751  ndmima  5105  iotass  5296  dffo2  5554  dff1o2  5579  resdif  5596  f1o00  5610  ressnop0  5824  fsnunfv  5844  ovid  6127  ovidig  6128  f1stres  6311  f2ndres  6312  rdgon  6538  elixpsn  6890  diffisn  7063  diffifi  7064  unsnfi  7092  snexxph  7128  ordiso2  7213  omp1eomlem  7272  ltexnqq  7606  enq0sym  7630  prarloclem5  7698  nqprloc  7743  nqprl  7749  nqpru  7750  pitonn  8046  axcnre  8079  peano5nnnn  8090  axcaucvglemres  8097  le2tri3i  8266  muldivdirap  8865  peano5nni  9124  0nn0  9395  uzind4  9795  elfz4  10226  eluzfz  10228  ssfzo12bi  10443  ioom  10492  ser0  10767  exp3vallem  10774  hashinfuni  11011  hashxp  11061  wrdsymb1  11121  ccatfv0  11151  lswccats1fst  11190  ccatswrd  11217  ccatpfx  11248  nn0abscl  11611  fimaxre2  11753  iserle  11868  climserle  11871  summodclem2a  11907  fsumcl2lem  11924  fsumadd  11932  sumsnf  11935  isumclim3  11949  isumadd  11957  sumsplitdc  11958  fsummulc2  11974  cvgcmpub  12002  isumshft  12016  isumlessdc  12022  trireciplem  12026  geolim  12037  geo2lim  12042  cvgratz  12058  mertenslem2  12062  mertensabs  12063  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodmul  12117  prodsnf  12118  ef0lem  12186  efcvgfsum  12193  ege2le3  12197  efcj  12199  efgt1p2  12221  ndvdsadd  12457  gcdsupex  12493  gcdsupcl  12494  ialgrlemconst  12580  divgcdcoprmex  12639  1idssfct  12652  odzdvds  12783  nninfdclemp1  13036  divsfval  13376  xpsfrnel2  13394  xpsff1o  13397  mulgnndir  13703  rmodislmodlem  14329  rmodislmod  14330  tgcl  14753  txcnp  14960  ivthdich  15342  plyval  15421  lgsval2lem  15704  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  lgsmodeq  15739  lgsmulsqcoprm  15740  2lgs  15798  bj-charfunbi  16229  bj-sucexg  16340  bj-indind  16350  bj-2inf  16356  findset  16363  trilpolemisumle  16466  nconstwlpolem0  16491