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  628  pm3.44  668  orbi2i  712  pm2.31  718  dcor  877  rnlem  918  syl3an1br  1209  syl3an2br  1210  syl3an3br  1211  xorbin  1316  3impexpbicom  1368  equveli  1683  sbbii  1689  dveeq2or  1738  exmoeudc  2005  eueq2dc  2766  ralun  3155  undif3ss  3232  ssunieq  3642  a9evsep  3908  tfi  4331  peano5  4347  opelxpi  4402  ndmima  4732  iotass  4914  dffo2  5141  dff1o2  5162  resdif  5179  f1o00  5192  ressnop0  5376  fsnunfv  5395  ovid  5648  ovidig  5649  f1stres  5817  f2ndres  5818  rdgon  6035  diffisn  6427  diffifi  6428  unsnfi  6439  ordiso2  6505  ltexnqq  6660  enq0sym  6684  prarloclem5  6752  nqprloc  6797  nqprl  6803  nqpru  6804  pitonn  7078  axcnre  7109  peano5nnnn  7120  axcaucvglemres  7127  le2tri3i  7286  muldivdirap  7862  peano5nni  8109  0nn0  8370  uzind4  8757  elfz4  9114  eluzfz  9116  ssfzo12bi  9311  ioom  9347  iser0  9568  sizeinfuni  9801  nn0abscl  10109  fimaxre2  10247  iserile  10318  ndvdsadd  10475  gcdsupex  10493  gcdsupcl  10494  ialgrlemconst  10569  divgcdcoprmex  10628  1idssfct  10641  bj-sucexg  10871  bj-indind  10885  bj-2inf  10891  findset  10898