Theorem biimpri 131

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 130	. 2 |- ( ps <-> ph )
3	2	biimpi 118	1 |- ( ps -> ph )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylibr  132  sylbir  133  sylbbr  134  sylbb1  135  sylbb2  136  mpbir  144  syl5bir  151  syl6ibr  160  bitri  182  sylanbr  279  sylan2br  282  simplbi2  377  sylanblrc  407  mtbi  627  pm3.44  667  orbi2i  711  pm2.31  717  dcor  876  rnlem  917  syl3an1br  1208  syl3an2br  1209  syl3an3br  1210  xorbin  1315  3impexpbicom  1367  equveli  1682  sbbii  1688  dveeq2or  1737  exmoeudc  2004  eueq2dc  2765  ralun  3154  undif3ss  3225  ssunieq  3634  a9evsep  3900  tfi  4323  peano5  4339  opelxpi  4394  ndmima  4722  iotass  4904  dffo2  5130  dff1o2  5151  resdif  5168  f1o00  5181  ressnop0  5365  fsnunfv  5384  ovid  5637  ovidig  5638  f1stres  5806  f2ndres  5807  diffisn  6377  diffifi  6378  unsnfi  6384  ordiso2  6446  ltexnqq  6598  enq0sym  6622  prarloclem5  6690  nqprloc  6735  nqprl  6741  nqpru  6742  pitonn  7016  axcnre  7047  peano5nnnn  7058  axcaucvglemres  7065  le2tri3i  7219  muldivdirap  7795  peano5nni  8042  0nn0  8303  uzind4  8676  elfz4  9038  eluzfz  9040  ssfzo12bi  9234  ioom  9269  iser0  9471  nn0abscl  9971  fimaxre2  10109  iserile  10180  ndvdsadd  10331  gcdsupex  10349  gcdsupcl  10350  ialgrlemconst  10425  divgcdcoprmex  10484  1idssfct  10497  bj-sucexg  10713  bj-indind  10727  bj-2inf  10733  findset  10740