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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  biranri  388  bilanri  389  sylanblrc  420  mtbi  681  pm3.44  727  orbi2i  774  pm2.31  780  dcor  948  rnlem  989  syl3an1br  1317  syl3an2br  1318  syl3an3br  1319  xorbin  1433  3impexpbicom  1488  equveli  1812  sbbii  1818  dveeq2or  1869  exmoeudc  2150  nfabdw  2411  eueq2dc  2999  ralun  3411  undif3ss  3492  ssunieq  3968  a9evsep  4255  uniex2  4581  dcextest  4728  tfi  4729  peano5  4745  opelxpi  4806  ndmima  5164  iotass  5355  dffo2  5619  dff1o2  5644  resdif  5661  f1o00  5676  ressnop0  5896  fsnunfv  5916  ovid  6205  ovidig  6206  f1stres  6393  f2ndres  6394  rdgon  6657  elixpsn  7017  modom  7108  diffisn  7197  diffifi  7198  unsnfi  7226  snexxph  7267  ordiso2  7375  omp1eomlem  7434  ltexnqq  7775  enq0sym  7799  prarloclem5  7867  nqprloc  7912  nqprl  7918  nqpru  7919  pitonn  8215  axcnre  8248  peano5nnnn  8259  axcaucvglemres  8266  le2tri3i  8435  muldivdirap  9039  peano5nni  9309  0nn0  9582  uzind4  9997  elfz4  10431  eluzfz  10433  ssfzo12bi  10653  ioom  10705  ser0  10983  exp3vallem  10990  hashinfuni  11230  hashxp  11281  wrdsymb1  11355  ccatfv0  11385  lswccats1fst  11426  ccatswrd  11456  ccatpfx  11487  nn0abscl  11866  fimaxre2  12008  iserle  12124  climserle  12127  summodclem2a  12164  fsumcl2lem  12181  fsumadd  12189  sumsnf  12192  isumclim3  12206  isumadd  12214  sumsplitdc  12215  fsummulc2  12231  cvgcmpub  12259  isumshft  12273  isumlessdc  12279  trireciplem  12283  geolim  12294  geo2lim  12299  cvgratz  12315  mertenslem2  12319  mertensabs  12320  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodmul  12374  prodsnf  12375  ef0lem  12443  efcvgfsum  12450  ege2le3  12454  efcj  12456  efgt1p2  12478  ndvdsadd  12714  gcdsupex  12750  gcdsupcl  12751  ialgrlemconst  12837  divgcdcoprmex  12896  1idssfct  12909  odzdvds  13044  nninfdclemp1  13390  divsfval  13698  xpsfrnel2  13716  xpsff1o  13719  mulgnndir  14003  opprdrng  14669  rmodislmodlem  14736  rmodislmod  14737  isassa  15051  tgcl  15214  txcnp  15421  ivthdich  15803  plyval  15882  logfac  16048  lgsval2lem  16227  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsmodeq  16262  lgsmulsqcoprm  16263  2lgs  16321  bj-charfunbi  16935  bj-sucexg  17046  bj-indind  17056  bj-2inf  17062  findset  17069  trilpolemisumle  17185  nconstwlpolem0  17211