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	|- (ph <-> ps)

Assertion

Ref	Expression
biimpri	|- (ps -> ph)

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 |- (ph <-> ps)
2	1	bicomi 193	. 2 |- (ps <-> ph)
3	2	biimpi 186	1 |- (ps -> ph)

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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  3011  ralun  3446  ssunieq  3925  cnvkexg  4287  p6exg  4291  ssetkex  4295  sikexg  4297  ins2kexg  4306  ins3kexg  4307  peano5  4410  ltfinirr  4458  spfininduct  4541  vfinspnn  4542  opbrop  4842  ndmima  5026  dminss  5042  dffo2  5274  dff1o2  5292  resdif  5307  f1o00  5318  ressnop0  5437  ovg  5602  clos1induct  5881  ssetpov  5945  nenpw1pwlem2  6086  sbthlem1  6204