Theorem biimpri 124

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 123	. 2 ⊢ (ψ ↔ φ)
3	2	biimpi 113	1 ⊢ (ψ → φ)

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sylbir  125  mpbir  134  sylibr  137  syl5bir  142  syl6ibr  151  bitri  173  sylanbr  269  sylan2br  272  simplbi2  367  mtbi  594  pm3.44  634  orbi2i  678  pm2.31  684  dcor  842  rnlem  882  syl3an1br  1173  syl3an2br  1174  syl3an3br  1175  xorbin  1272  3impexpbicom  1324  equveli  1639  sbbii  1645  dveeq2or  1694  exmoeudc  1960  eueq2dc  2708  ralun  3119  undif3ss  3192  ssunieq  3604  a9evsep  3870  tfi  4248  peano5  4264  opelxpi  4319  ndmima  4645  iotass  4827  dffo2  5053  dff1o2  5074  resdif  5091  f1o00  5104  ressnop0  5287  fsnunfv  5306  ovid  5559  ovidig  5560  f1stres  5728  f2ndres  5729  ltexnqq  6391  enq0sym  6415  prarloclem5  6483  nqprloc  6528  nqprl  6533  pitonn  6744  axcnre  6765  le2tri3i  6923  peano5nni  7698  0nn0  7972  uzind4  8307  elfz4  8653  eluzfz  8655  ssfzo12bi  8851  nn0abscl  9229  bj-sucexg  9377  bj-indind  9391  bj-2inf  9397  peano5setOLD  9400  findset  9405