Theorem biimpri 133

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylibr  134  sylbir  135  sylbbr  136  sylbb1  137  sylbb2  138  mpbir  146  biimtrrid  153  imbitrrdi  162  bitri  184  sylanbr  285  sylan2br  288  simplbi2  385  sylanblrc  416  mtbi  677  pm3.44  723  orbi2i  770  pm2.31  776  dcor  944  rnlem  985  syl3an1br  1313  syl3an2br  1314  syl3an3br  1315  xorbin  1429  3impexpbicom  1484  equveli  1808  sbbii  1814  dveeq2or  1865  exmoeudc  2146  nfabdw  2405  eueq2dc  2993  ralun  3405  undif3ss  3486  ssunieq  3952  a9evsep  4237  dcextest  4708  tfi  4709  peano5  4725  opelxpi  4786  ndmima  5144  iotass  5335  dffo2  5599  dff1o2  5624  resdif  5641  f1o00  5656  ressnop0  5870  fsnunfv  5890  ovid  6178  ovidig  6179  f1stres  6366  f2ndres  6367  rdgon  6630  elixpsn  6983  modom  7074  diffisn  7163  diffifi  7164  unsnfi  7192  snexxph  7233  ordiso2  7339  omp1eomlem  7398  ltexnqq  7739  enq0sym  7763  prarloclem5  7831  nqprloc  7876  nqprl  7882  nqpru  7883  pitonn  8179  axcnre  8212  peano5nnnn  8223  axcaucvglemres  8230  le2tri3i  8398  muldivdirap  8998  peano5nni  9257  0nn0  9528  uzind4  9938  elfz4  10371  eluzfz  10373  ssfzo12bi  10592  ioom  10644  ser0  10919  exp3vallem  10926  hashinfuni  11165  hashxp  11216  wrdsymb1  11286  ccatfv0  11316  lswccats1fst  11357  ccatswrd  11387  ccatpfx  11418  nn0abscl  11795  fimaxre2  11937  iserle  12052  climserle  12055  summodclem2a  12092  fsumcl2lem  12109  fsumadd  12117  sumsnf  12120  isumclim3  12134  isumadd  12142  sumsplitdc  12143  fsummulc2  12159  cvgcmpub  12187  isumshft  12201  isumlessdc  12207  trireciplem  12211  geolim  12222  geo2lim  12227  cvgratz  12243  mertenslem2  12247  mertensabs  12248  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodmul  12302  prodsnf  12303  ef0lem  12371  efcvgfsum  12378  ege2le3  12382  efcj  12384  efgt1p2  12406  ndvdsadd  12642  gcdsupex  12678  gcdsupcl  12679  ialgrlemconst  12765  divgcdcoprmex  12824  1idssfct  12837  odzdvds  12968  nninfdclemp1  13285  divsfval  13592  xpsfrnel2  13610  xpsff1o  13613  mulgnndir  13904  opprdrng  14558  rmodislmodlem  14624  rmodislmod  14625  tgcl  15055  txcnp  15262  ivthdich  15644  plyval  15723  lgsval2lem  16009  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsmodeq  16044  lgsmulsqcoprm  16045  2lgs  16103  bj-charfunbi  16707  bj-sucexg  16818  bj-indind  16828  bj-2inf  16834  findset  16841  trilpolemisumle  16948  nconstwlpolem0  16975