Theorem biimpri 131

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylibr  132  sylbir  133  sylbbr  134  sylbb1  135  sylbb2  136  mpbir  144  syl5bir  151  syl6ibr  160  bitri  182  sylanbr  279  sylan2br  282  simplbi2  377  sylanblrc  407  mtbi  628  pm3.44  668  orbi2i  712  pm2.31  718  dcor  879  rnlem  920  syl3an1br  1211  syl3an2br  1212  syl3an3br  1213  xorbin  1318  3impexpbicom  1370  equveli  1686  sbbii  1692  dveeq2or  1741  exmoeudc  2008  eueq2dc  2778  ralun  3168  undif3ss  3246  ssunieq  3663  a9evsep  3929  dcextest  4362  tfi  4363  peano5  4379  opelxpi  4435  ndmima  4767  iotass  4954  dffo2  5188  dff1o2  5209  resdif  5226  f1o00  5239  ressnop0  5423  fsnunfv  5442  ovid  5699  ovidig  5700  f1stres  5868  f2ndres  5869  rdgon  6086  diffisn  6542  diffifi  6543  unsnfi  6559  snexxph  6586  ordiso2  6649  ltexnqq  6888  enq0sym  6912  prarloclem5  6980  nqprloc  7025  nqprl  7031  nqpru  7032  pitonn  7306  axcnre  7337  peano5nnnn  7348  axcaucvglemres  7355  le2tri3i  7514  muldivdirap  8090  peano5nni  8337  0nn0  8598  uzind4  8985  elfz4  9342  eluzfz  9344  ssfzo12bi  9539  ioom  9575  iser0  9801  hashinfuni  10034  hashxp  10083  nn0abscl  10359  fimaxre2  10497  iserile  10568  ndvdsadd  10725  gcdsupex  10743  gcdsupcl  10744  ialgrlemconst  10819  divgcdcoprmex  10878  1idssfct  10891  bj-sucexg  11170  bj-indind  11184  bj-2inf  11190  findset  11197