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  676  pm3.44  722  orbi2i  769  pm2.31  775  dcor  943  rnlem  984  syl3an1br  1312  syl3an2br  1313  syl3an3br  1314  xorbin  1428  3impexpbicom  1483  equveli  1807  sbbii  1813  dveeq2or  1864  exmoeudc  2143  nfabdw  2393  eueq2dc  2979  ralun  3389  undif3ss  3468  ssunieq  3926  a9evsep  4211  dcextest  4679  tfi  4680  peano5  4696  opelxpi  4757  ndmima  5113  iotass  5304  dffo2  5563  dff1o2  5588  resdif  5605  f1o00  5620  ressnop0  5835  fsnunfv  5855  ovid  6138  ovidig  6139  f1stres  6322  f2ndres  6323  rdgon  6552  elixpsn  6904  modom  6994  diffisn  7082  diffifi  7083  unsnfi  7111  snexxph  7149  ordiso2  7234  omp1eomlem  7293  ltexnqq  7628  enq0sym  7652  prarloclem5  7720  nqprloc  7765  nqprl  7771  nqpru  7772  pitonn  8068  axcnre  8101  peano5nnnn  8112  axcaucvglemres  8119  le2tri3i  8288  muldivdirap  8887  peano5nni  9146  0nn0  9417  uzind4  9822  elfz4  10253  eluzfz  10255  ssfzo12bi  10471  ioom  10521  ser0  10796  exp3vallem  10803  hashinfuni  11040  hashxp  11091  wrdsymb1  11154  ccatfv0  11184  lswccats1fst  11225  ccatswrd  11255  ccatpfx  11286  nn0abscl  11663  fimaxre2  11805  iserle  11920  climserle  11923  summodclem2a  11960  fsumcl2lem  11977  fsumadd  11985  sumsnf  11988  isumclim3  12002  isumadd  12010  sumsplitdc  12011  fsummulc2  12027  cvgcmpub  12055  isumshft  12069  isumlessdc  12075  trireciplem  12079  geolim  12090  geo2lim  12095  cvgratz  12111  mertenslem2  12115  mertensabs  12116  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodmul  12170  prodsnf  12171  ef0lem  12239  efcvgfsum  12246  ege2le3  12250  efcj  12252  efgt1p2  12274  ndvdsadd  12510  gcdsupex  12546  gcdsupcl  12547  ialgrlemconst  12633  divgcdcoprmex  12692  1idssfct  12705  odzdvds  12836  nninfdclemp1  13089  divsfval  13429  xpsfrnel2  13447  xpsff1o  13450  mulgnndir  13756  rmodislmodlem  14383  rmodislmod  14384  tgcl  14807  txcnp  15014  ivthdich  15396  plyval  15475  lgsval2lem  15758  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgsmodeq  15793  lgsmulsqcoprm  15794  2lgs  15852  bj-charfunbi  16457  bj-sucexg  16568  bj-indind  16578  bj-2inf  16584  findset  16591  trilpolemisumle  16693  nconstwlpolem0  16719