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  6414  prarloclem5  6482  nqprloc  6528  pitonn  6704  axcnre  6725  le2tri3i  6883  peano5nni  7658  0nn0  7932  uzind4  8267  elfz4  8613  eluzfz  8615  ssfzo12bi  8811  bj-sucexg  9307  bj-2inf  9326  peano5set  9328  findset  9333