Theorem biimpri 132

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 131	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 119	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylibr  133  sylbir  134  sylbbr  135  sylbb1  136  sylbb2  137  mpbir  145  syl5bir  152  syl6ibr  161  bitri  183  sylanbr  281  sylan2br  284  simplbi2  380  sylanblrc  410  mtbi  636  pm3.44  676  orbi2i  720  pm2.31  726  dcor  887  rnlem  928  syl3an1br  1223  syl3an2br  1224  syl3an3br  1225  xorbin  1330  3impexpbicom  1382  equveli  1700  sbbii  1706  dveeq2or  1755  exmoeudc  2023  eueq2dc  2810  ralun  3205  undif3ss  3284  ssunieq  3716  a9evsep  3990  dcextest  4433  tfi  4434  peano5  4450  opelxpi  4509  ndmima  4852  iotass  5041  dffo2  5285  dff1o2  5306  resdif  5323  f1o00  5336  ressnop0  5533  fsnunfv  5553  ovid  5819  ovidig  5820  f1stres  5988  f2ndres  5989  rdgon  6213  elixpsn  6559  diffisn  6716  diffifi  6717  unsnfi  6736  snexxph  6766  ordiso2  6835  omp1eomlem  6894  ltexnqq  7117  enq0sym  7141  prarloclem5  7209  nqprloc  7254  nqprl  7260  nqpru  7261  pitonn  7535  axcnre  7566  peano5nnnn  7577  axcaucvglemres  7584  le2tri3i  7743  muldivdirap  8328  peano5nni  8581  0nn0  8844  uzind4  9233  elfz4  9640  eluzfz  9642  ssfzo12bi  9843  ioom  9879  ser0  10128  exp3vallem  10135  hashinfuni  10364  hashxp  10413  nn0abscl  10697  fimaxre2  10837  iserle  10950  climserle  10953  summodclem2a  10989  fsumcl2lem  11006  fsumadd  11014  sumsnf  11017  isumclim3  11031  isumadd  11039  sumsplitdc  11040  fsummulc2  11056  cvgcmpub  11084  isumshft  11098  isumlessdc  11104  trireciplem  11108  geolim  11119  geo2lim  11124  cvgratz  11140  mertenslem2  11144  mertensabs  11145  ef0lem  11164  efcvgfsum  11171  ege2le3  11175  efcj  11177  efgt1p2  11199  ndvdsadd  11423  gcdsupex  11441  gcdsupcl  11442  ialgrlemconst  11517  divgcdcoprmex  11576  1idssfct  11589  tgcl  12015  txcnp  12221  bj-sucexg  12701  bj-indind  12715  bj-2inf  12721  findset  12728  trilpolemisumle  12815