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  670  pm3.44  715  orbi2i  762  pm2.31  768  dcor  935  rnlem  976  syl3an1br  1277  syl3an2br  1278  syl3an3br  1279  xorbin  1384  3impexpbicom  1438  equveli  1759  sbbii  1765  dveeq2or  1816  exmoeudc  2089  nfabdw  2338  eueq2dc  2912  ralun  3319  undif3ss  3398  ssunieq  3844  a9evsep  4127  dcextest  4582  tfi  4583  peano5  4599  opelxpi  4660  ndmima  5007  iotass  5197  dffo2  5444  dff1o2  5468  resdif  5485  f1o00  5498  ressnop0  5699  fsnunfv  5719  ovid  5993  ovidig  5994  f1stres  6162  f2ndres  6163  rdgon  6389  elixpsn  6737  diffisn  6895  diffifi  6896  unsnfi  6920  snexxph  6951  ordiso2  7036  omp1eomlem  7095  ltexnqq  7409  enq0sym  7433  prarloclem5  7501  nqprloc  7546  nqprl  7552  nqpru  7553  pitonn  7849  axcnre  7882  peano5nnnn  7893  axcaucvglemres  7900  le2tri3i  8068  muldivdirap  8666  peano5nni  8924  0nn0  9193  uzind4  9590  elfz4  10020  eluzfz  10022  ssfzo12bi  10227  ioom  10263  ser0  10516  exp3vallem  10523  hashinfuni  10759  hashxp  10808  nn0abscl  11096  fimaxre2  11237  iserle  11352  climserle  11355  summodclem2a  11391  fsumcl2lem  11408  fsumadd  11416  sumsnf  11419  isumclim3  11433  isumadd  11441  sumsplitdc  11442  fsummulc2  11458  cvgcmpub  11486  isumshft  11500  isumlessdc  11506  trireciplem  11510  geolim  11521  geo2lim  11526  cvgratz  11542  mertenslem2  11546  mertensabs  11547  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodmul  11601  prodsnf  11602  ef0lem  11670  efcvgfsum  11677  ege2le3  11681  efcj  11683  efgt1p2  11705  ndvdsadd  11938  gcdsupex  11960  gcdsupcl  11961  ialgrlemconst  12045  divgcdcoprmex  12104  1idssfct  12117  odzdvds  12247  nninfdclemp1  12453  xpsfrnel2  12770  xpsff1o  12773  mulgnndir  13017  rmodislmodlem  13445  rmodislmod  13446  tgcl  13649  txcnp  13856  lgsval2lem  14496  lgsdir  14521  lgsdilem2  14522  lgsdi  14523  lgsne0  14524  lgsmodeq  14531  lgsmulsqcoprm  14532  bj-charfunbi  14648  bj-sucexg  14759  bj-indind  14769  bj-2inf  14775  findset  14782  trilpolemisumle  14871  nconstwlpolem0  14896