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  672  pm3.44  717  orbi2i  764  pm2.31  770  dcor  938  rnlem  979  syl3an1br  1289  syl3an2br  1290  syl3an3br  1291  xorbin  1404  3impexpbicom  1459  equveli  1783  sbbii  1789  dveeq2or  1840  exmoeudc  2118  nfabdw  2368  eueq2dc  2950  ralun  3359  undif3ss  3438  ssunieq  3889  a9evsep  4174  dcextest  4637  tfi  4638  peano5  4654  opelxpi  4715  ndmima  5068  iotass  5258  dffo2  5514  dff1o2  5539  resdif  5556  f1o00  5570  ressnop0  5778  fsnunfv  5798  ovid  6075  ovidig  6076  f1stres  6258  f2ndres  6259  rdgon  6485  elixpsn  6835  diffisn  7005  diffifi  7006  unsnfi  7031  snexxph  7067  ordiso2  7152  omp1eomlem  7211  ltexnqq  7541  enq0sym  7565  prarloclem5  7633  nqprloc  7678  nqprl  7684  nqpru  7685  pitonn  7981  axcnre  8014  peano5nnnn  8025  axcaucvglemres  8032  le2tri3i  8201  muldivdirap  8800  peano5nni  9059  0nn0  9330  uzind4  9729  elfz4  10160  eluzfz  10162  ssfzo12bi  10376  ioom  10425  ser0  10700  exp3vallem  10707  hashinfuni  10944  hashxp  10993  wrdsymb1  11052  ccatfv0  11082  lswccats1fst  11119  ccatswrd  11146  ccatpfx  11177  nn0abscl  11471  fimaxre2  11613  iserle  11728  climserle  11731  summodclem2a  11767  fsumcl2lem  11784  fsumadd  11792  sumsnf  11795  isumclim3  11809  isumadd  11817  sumsplitdc  11818  fsummulc2  11834  cvgcmpub  11862  isumshft  11876  isumlessdc  11882  trireciplem  11886  geolim  11897  geo2lim  11902  cvgratz  11918  mertenslem2  11922  mertensabs  11923  prodmodclem3  11961  prodmodclem2a  11962  zproddc  11965  fprodmul  11977  prodsnf  11978  ef0lem  12046  efcvgfsum  12053  ege2le3  12057  efcj  12059  efgt1p2  12081  ndvdsadd  12317  gcdsupex  12353  gcdsupcl  12354  ialgrlemconst  12440  divgcdcoprmex  12499  1idssfct  12512  odzdvds  12643  nninfdclemp1  12896  divsfval  13235  xpsfrnel2  13253  xpsff1o  13256  mulgnndir  13562  rmodislmodlem  14187  rmodislmod  14188  tgcl  14611  txcnp  14818  ivthdich  15200  plyval  15279  lgsval2lem  15562  lgsdir  15587  lgsdilem2  15588  lgsdi  15589  lgsne0  15590  lgsmodeq  15597  lgsmulsqcoprm  15598  2lgs  15656  bj-charfunbi  15885  bj-sucexg  15996  bj-indind  16006  bj-2inf  16012  findset  16019  trilpolemisumle  16118  nconstwlpolem0  16143