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-mp 5  ax-1 6  ax-2 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  283  sylan2br  286  simplbi2  382  sylanblrc  412  mtbi  659  pm3.44  704  orbi2i  751  pm2.31  757  dcor  919  rnlem  960  syl3an1br  1255  syl3an2br  1256  syl3an3br  1257  xorbin  1362  3impexpbicom  1414  equveli  1732  sbbii  1738  dveeq2or  1788  exmoeudc  2062  eueq2dc  2857  ralun  3258  undif3ss  3337  ssunieq  3769  a9evsep  4050  dcextest  4495  tfi  4496  peano5  4512  opelxpi  4571  ndmima  4916  iotass  5105  dffo2  5349  dff1o2  5372  resdif  5389  f1o00  5402  ressnop0  5601  fsnunfv  5621  ovid  5887  ovidig  5888  f1stres  6057  f2ndres  6058  rdgon  6283  elixpsn  6629  diffisn  6787  diffifi  6788  unsnfi  6807  snexxph  6838  ordiso2  6920  omp1eomlem  6979  ltexnqq  7216  enq0sym  7240  prarloclem5  7308  nqprloc  7353  nqprl  7359  nqpru  7360  pitonn  7656  axcnre  7689  peano5nnnn  7700  axcaucvglemres  7707  le2tri3i  7872  muldivdirap  8467  peano5nni  8723  0nn0  8992  uzind4  9383  elfz4  9799  eluzfz  9801  ssfzo12bi  10002  ioom  10038  ser0  10287  exp3vallem  10294  hashinfuni  10523  hashxp  10572  nn0abscl  10857  fimaxre2  10998  iserle  11111  climserle  11114  summodclem2a  11150  fsumcl2lem  11167  fsumadd  11175  sumsnf  11178  isumclim3  11192  isumadd  11200  sumsplitdc  11201  fsummulc2  11217  cvgcmpub  11245  isumshft  11259  isumlessdc  11265  trireciplem  11269  geolim  11280  geo2lim  11285  cvgratz  11301  mertenslem2  11305  mertensabs  11306  prodmodclem3  11344  prodmodclem2a  11345  ef0lem  11366  efcvgfsum  11373  ege2le3  11377  efcj  11379  efgt1p2  11401  ndvdsadd  11628  gcdsupex  11646  gcdsupcl  11647  ialgrlemconst  11724  divgcdcoprmex  11783  1idssfct  11796  tgcl  12233  txcnp  12440  bj-sucexg  13120  bj-indind  13130  bj-2inf  13136  findset  13143  trilpolemisumle  13231