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  pm3.43OLD  523  mtbi  582  pm3.44  622  orbi2i  666  pm2.31  672  dcor  831  rnlem  871  syl3an1br  1160  syl3an2br  1161  syl3an3br  1162  xorbin  1258  3impexpbicom  1306  equveli  1624  sbbii  1630  dveeq2or  1679  exmoeudc  1945  eueq2dc  2691  ralun  3102  undif3ss  3175  ssunieq  3587  a9evsep  3853  suctr  4108  tfi  4232  peano5  4248  opelxpi  4303  ndmima  4629  iotass  4811  dffo2  5035  dff1o2  5056  resdif  5073  f1o00  5086  ressnop0  5269  fsnunfv  5288  ovid  5540  ovidig  5541  f1stres  5709  f2ndres  5710  frec0g  5902  ltexnqq  6266  enq0sym  6287  prarloclem5  6354  nqprloc  6400  axcnre  6575  bj-sucexg  7145  bj-2inf  7160  peano5set  7162  findset  7167