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  672  pm3.44  717  orbi2i  764  pm2.31  770  dcor  938  rnlem  979  syl3an1br  1289  syl3an2br  1290  syl3an3br  1291  xorbin  1404  3impexpbicom  1458  equveli  1782  sbbii  1788  dveeq2or  1839  exmoeudc  2117  nfabdw  2367  eueq2dc  2946  ralun  3355  undif3ss  3434  ssunieq  3883  a9evsep  4167  dcextest  4630  tfi  4631  peano5  4647  opelxpi  4708  ndmima  5060  iotass  5250  dffo2  5504  dff1o2  5529  resdif  5546  f1o00  5559  ressnop0  5767  fsnunfv  5787  ovid  6064  ovidig  6065  f1stres  6247  f2ndres  6248  rdgon  6474  elixpsn  6824  diffisn  6992  diffifi  6993  unsnfi  7018  snexxph  7054  ordiso2  7139  omp1eomlem  7198  ltexnqq  7523  enq0sym  7547  prarloclem5  7615  nqprloc  7660  nqprl  7666  nqpru  7667  pitonn  7963  axcnre  7996  peano5nnnn  8007  axcaucvglemres  8014  le2tri3i  8183  muldivdirap  8782  peano5nni  9041  0nn0  9312  uzind4  9711  elfz4  10142  eluzfz  10144  ssfzo12bi  10356  ioom  10405  ser0  10680  exp3vallem  10687  hashinfuni  10924  hashxp  10973  wrdsymb1  11032  ccatfv0  11062  lswccats1fst  11099  ccatswrd  11126  ccatpfx  11155  nn0abscl  11429  fimaxre2  11571  iserle  11686  climserle  11689  summodclem2a  11725  fsumcl2lem  11742  fsumadd  11750  sumsnf  11753  isumclim3  11767  isumadd  11775  sumsplitdc  11776  fsummulc2  11792  cvgcmpub  11820  isumshft  11834  isumlessdc  11840  trireciplem  11844  geolim  11855  geo2lim  11860  cvgratz  11876  mertenslem2  11880  mertensabs  11881  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodmul  11935  prodsnf  11936  ef0lem  12004  efcvgfsum  12011  ege2le3  12015  efcj  12017  efgt1p2  12039  ndvdsadd  12275  gcdsupex  12311  gcdsupcl  12312  ialgrlemconst  12398  divgcdcoprmex  12457  1idssfct  12470  odzdvds  12601  nninfdclemp1  12854  divsfval  13193  xpsfrnel2  13211  xpsff1o  13214  mulgnndir  13520  rmodislmodlem  14145  rmodislmod  14146  tgcl  14569  txcnp  14776  ivthdich  15158  plyval  15237  lgsval2lem  15520  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgsmodeq  15555  lgsmulsqcoprm  15556  2lgs  15614  bj-charfunbi  15784  bj-sucexg  15895  bj-indind  15905  bj-2inf  15911  findset  15918  trilpolemisumle  16014  nconstwlpolem0  16039