Theorem biimpri 197

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

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  mpbir  200  sylibr  203  sylbir  204  syl5bir  209  syl6ibr  218  bitri  240  mtbi  289  pm2.54  363  sylanbr  459  sylan2br  462  pm3.11  485  orbi2i  505  pm2.31  511  simplbi2  608  dfbi  610  pm2.85  826  rnlem  931  syl3an1br  1221  syl3an2br  1222  syl3an3br  1223  3impexpbicom  1367  nic-axALT  1439  sbbii  1653  hbn1fw  1705  equveli  1988  exmoeu  2246  eueq2  3010  ralun  3445  ssunieq  3924  cnvkexg  4286  p6exg  4290  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  peano5  4409  ltfinirr  4457  spfininduct  4540  vfinspnn  4541  opbrop  4841  ndmima  5025  dminss  5041  dffo2  5273  dff1o2  5291  resdif  5306  f1o00  5317  ressnop0  5436  ovg  5601  clos1induct  5880  ssetpov  5944  nenpw1pwlem2  6085  sbthlem1  6203