Theorem impbii 188

Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 29-Dec-1992.)

Hypotheses

Ref	Expression
impbii.1
impbii.2

Assertion

Ref	Expression
impbii

Proof of Theorem impbii

Step	Hyp	Ref	Expression
1		impbii.1	. 2
2		impbii.2	. 2
3		bi3 187	. 2
4	1, 2, 3	mp2 9	1

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

This theorem is referenced by:  dfbi1  192  bicom  200  biid  236  2th  239  pm5.74  244  bitri  249  notnot  291  con34b  292  notbi  295  bibi2i  313  con1b  333  con2b  334  bi2.04  361  pm5.4  362  imdi  363  pm4.8  365  pm4.81  366  orcom  387  dfor2  411  impexp  446  ancom  450  oridm  514  orbi2i  519  or12  523  pm4.45im  562  pm4.44  577  pm4.79  583  anass  649  jaob  783  jcab  863  andi  867  pm4.72  876  oibabs  881  pm4.82  928  consensus  959  rnlemOLD  965  cases2  971  3jaob  1290  truanOLD  1413  dfnotOLD  1415  cad1  1465  tbw-bijust  1531  tbw-negdf  1532  19.26  1680  19.35  1687  19.21v  1729  sbbii  1746  19.9v  1754  19.23v  1760  19.41v  1771  equcom  1794  equvin  1804  cbvalw  1808  alcom  1845  19.3  1888  19.41  1971  cbval  2021  equsex  2038  aecom  2051  equvinOLD  2090  equs45f  2091  dfsb2  2114  sb6f  2126  sbim  2136  sb6  2173  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  exmoeu  2316  mo3  2323  mo3OLD  2324  mo2OLD  2334  moanim  2350  euan  2351  2mo  2373  2moOLD  2374  2eu6  2383  2eu6OLD  2384  axext4  2439  eqcom  2466  cleqhOLD  2573  nebi  2767  r19.26  2984  ralcom3  3023  ceqsex  3145  gencbvex  3153  gencbvex2  3154  eqvinc  3226  pm13.183  3240  rr19.3v  3241  rr19.28v  3242  euxfr2  3284  reu6  3288  reu3  3289  sspss  3602  unineq  3747  uneqin  3748  undif3  3758  difrab  3771  sbnfc2  3854  un00  3862  ssdifeq0  3910  r19.2zb  3919  ralf0  3936  elpr2  4048  snidb  4056  rabsnifsb  4098  tppreqb  4171  difsnb  4172  pwpw0  4178  sssn  4188  preq12b  4206  preqsn  4213  pwsnALT  4244  unissint  4311  uniintsn  4324  iununi  4415  intex  4608  intnex  4609  iin0  4626  axpweq  4629  eusvnfb  4648  eusv2nf  4650  ralxfrALT  4671  nfcvb  4682  sspwb  4701  unipw  4702  opnz  4723  opth  4726  opthwiener  4754  ssopab2b  4779  pwssun  4791  elon2  4894  opelxp  5034  opthprc  5052  relop  5158  issetid  5162  xpid11  5229  elres  5314  eldmeldmressn  5319  iss  5326  restidsing  5335  issref  5385  asymref2  5389  xpnz  5431  xpdifid  5440  ssrnres  5450  dfrel2  5462  relrelss  5536  unixp0  5546  fn0  5705  funssxp  5749  f00  5772  f0bi  5773  dffo2  5804  f1o00  5853  fo00  5854  fv3  5884  dffn5  5918  dff2  6043  dff3  6044  dffo4  6047  dffo5  6048  exfo  6049  fmpt  6052  ffnfv  6057  fsn  6069  fsn2  6071  fnsnb  6090  fconstfvOLD  6134  isores1  6230  ssoprab2b  6354  eqfnov2  6409  unexb  6600  uniexb  6610  iunpw  6614  ordeleqon  6624  onintrab  6636  unon  6666  onuninsuci  6675  ordzsl  6680  onzsl  6681  f1oexbi  6750  ffoss  6761  1st2ndb  6838  suppssov1  6951  suppssfv  6955  reldmtpos  6982  omopthi  7325  mapsn  7480  mapsncnv  7485  mptelixpg  7526  elixpsn  7528  ixpsnf1o  7529  bren2  7566  en0  7598  en1  7602  en1b  7603  sbthb  7658  canth2  7690  onfin2  7729  sdom1  7739  1sdom  7742  fineqv  7755  unfilem1  7804  fiint  7817  pwfi  7835  unifpw  7843  wofib  7991  sucprcreg  8046  sucprcregOLD  8047  opthreg  8056  suc11reg  8057  infeq5  8075  rankwflemb  8232  r1elss  8245  pwwf  8246  unwf  8249  uniwf  8258  rankonid  8268  rankr1id  8301  rankuni  8302  rankxplim3  8320  scott0  8325  karden  8334  isnum3  8356  oncard  8362  card1  8370  cardlim  8374  cardmin2  8400  pm54.43lem  8401  ween  8437  acnnum  8454  alephsuc2  8482  alephgeom  8484  iscard3  8495  dfac3  8523  dfac4  8524  dfac5lem3  8527  dfac5  8530  dfac2  8532  dfac8  8536  dfac9  8537  dfacacn  8542  dfac13  8543  dfac12r  8547  dfac12k  8548  kmlem2  8552  kmlem13  8563  cdainf  8593  ackbij2  8644  cflim2  8664  isfin4-2  8715  isfin4-3  8716  isf33lem  8767  compsscnv  8772  fin1a2lem6  8806  domtriom  8844  ac9  8884  ac9s  8894  fodomb  8925  brdom3  8927  brdom5  8928  brdom4  8929  brdom7disj  8930  brdom6disj  8931  iunfo  8935  sdomsdomcard  8956  gch2  9074  gch3  9075  eltsk2g  9150  grutsk  9221  grothpw  9225  ordpipq  9341  ltbtwnnq  9377  mappsrpr  9506  map2psrpr  9508  elreal2  9530  le2tri3i  9735  ltadd2iOLD  9737  elnn0nn  10863  elnnnn0b  10865  elnnnn0c  10866  elnnz  10899  elnn0z  10902  elz2  10906  elnnz1  10915  eluz2b2  11183  elnn1uz2  11187  elioo4g  11614  eluzfz2b  11724  fzn0  11729  elfz1end  11744  fzass4  11750  elfz1b  11777  nn0fz0  11803  fzolb  11834  fzon0  11845  elfzo0  11863  fzo1fzo0n0  11864  elfzo0z  11865  elfzo1  11871  om2uzrani  12063  nn0opthi  12350  hashkf  12407  hashprb  12462  hashf1  12506  iswrdbi  12554  wrdexb  12558  0wrd0  12566  sqr0lem  13074  rexanuz  13178  rexuz3  13181  fsum0diag  13592  fprod0diag  13790  sadcp1  14105  isprm6  14250  4sqlem4  14470  mreunirn  14998  isdrs2  15568  isacs5  15802  isacs4  15803  isacs3  15804  isnsg3  16235  gicer  16324  oppgmndb  16390  oppggrpb  16393  pmtrfb  16490  invghm  16842  opprringb  17281  isnzr2hash  17912  abvn0b  17951  funsnfsupOLD  18256  gzrngunit  18483  dvdsrzring  18507  dvdsrz  18508  zringunit  18520  zrngunit  18521  zlmlmod  18560  zlmassa  18561  cygth  18610  frgpcyg  18612  tgclb  19472  iscldtop  19596  isnrm2  19859  isnrm3  19860  discmp  19898  dfcon2  19920  2ndcsb  19950  dis2ndc  19961  loclly  19988  unisngl  20028  locfindis  20031  iskgen2  20049  dfac14  20119  kqtop  20246  kqt0  20247  kqreg  20252  kqnrm  20253  hmpher  20285  hmphsymb  20287  hmph0  20296  kqhmph  20320  ist1-5lem  20321  elmptrab2  20329  isfil2  20357  filunirn  20383  isufil2  20409  hausflim  20482  isfcls  20510  alexsubALT  20551  istgp2  20590  ustbas  20730  xmetunirn  20840  dscmet  21093  dscopn  21094  isngp4  21131  zcld  21318  zlmclm  21595  iscmet2  21733  iundisj  21958  i1f1lem  22096  fta1b  22570  elply2  22593  elqaa  22718  aannenlem2  22725  wilth  23345  lgsne0  23608  2sqlem2  23639  ostth  23824  mptelee  24198  uhgra0v  24310  wrdumgra  24316  usgra0v  24371  uvtx01vtx  24492  wlkcpr  24529  isspthonpth  24586  eclclwwlkn1  24832  usg2spthonot1  24890  clwlknclwlkdifs  24960  frgra0v  24993  nmlno0lem  25708  isblo3i  25716  blocni  25720  hvsubeq0i  25980  hvaddcani  25982  bcseqi  26037  isch3  26159  norm1exi  26168  hhsssh  26185  shslubi  26303  dfch2  26325  pjoc1i  26349  pjchi  26350  shs00i  26368  chsscon3i  26379  chlejb1i  26394  chj00i  26405  shjshseli  26411  h1de2ctlem  26473  spanunsni  26497  cmcmi  26510  cmbr3i  26518  cmbr4i  26519  pj11i  26629  hosubeq0i  26745  dmadjrnb  26825  nmlnop0iALT  26914  lnopeq0i  26926  elunop2  26932  lnconi  26952  lncnopbd  26956  adjbdlnb  27003  adjbd1o  27004  adjeq0  27010  rnbra  27026  pjss1coi  27082  pjss2coi  27083  pjnormssi  27087  pjssdif2i  27093  pjssdif1i  27094  dfpjop  27101  pjinvari  27110  pjin2i  27112  pjci  27119  pjcmul1i  27120  pjcmul2i  27121  strb  27177  hstrbi  27185  mdsl1i  27240  atom1d  27272  chrelat2i  27284  cvbr4i  27286  cvexchi  27288  sumdmdi  27339  dmdbr4ati  27340  dmdbr5ati  27341  dmdbr6ati  27342  dmdbr7ati  27343  cdj3i  27360  difeq  27416  iundisjf  27448  cnvoprab  27546  fpwrelmap  27556  iundisjfi  27601  xrge0tsmsbi  27776  issgon  28123  measbasedom  28173  oddpwdc  28293  eulerpartlemt  28310  ballotlem2  28427  ballotlemrinv  28472  elmsta  28908  nepss  29095  dfpo2  29184  dfon2  29224  distel  29236  elno2  29414  bdayfo  29435  fnimage  29579  altopthsn  29611  ellines  29802  rankeq1o  29828  df3nandALT1  29862  wl-nfnbi  29979  wl-exeq  29987  wl-aleq  29988  wl-nfeqfb  29990  wl-ax11-lem6  30030  volsupnfl  30059  dvtanlem  30064  opnrebl2  30139  cover2  30204  isbnd3  30280  cntotbnd  30292  heibor  30317  isfld2  30402  isfldidl  30465  orfa  30479  prtlem16  30610  ismrc  30633  isnacs3  30642  rexzrexnn0  30737  eldioph4b  30745  dford3  30970  wopprc  30972  ttac  30978  pw2f1ocnv  30979  dfac11  31008  dfac21  31012  isnumbasabl  31055  isnumbasgrp  31056  dfacbasgrp  31057  aaitgo  31111  nanorxor  31185  nzss  31222  pm10.55  31274  pm11.57  31295  sbeqalbi  31307  pm13.192  31317  pm13.194  31319  ipo0  31358  ifr0  31359  xpexb  31363  elfzfzo  31458  dvnprodlem3  31745  elaa2  32017  reuan  32185  afvfv0bi  32237  ffnafv  32256  residfi  32314  mgm2mgm  32551  isringrng  32687  3impexp  33220  3impexpbicom  33221  com3rgbi  33284  pm2.43bgbi  33287  pm2.43cbi  33288  sb5ALT  33295  trsbc  33311  2pm13.193  33325  ax6e2ndeq  33332  2uasbanh  33334  eelT01  33503  eel0T1  33504  uunT1  33577  zfregs2VD  33641  equncomVD  33668  trsbcVD  33677  undif3VD  33682  2pm13.193VD  33703  ax6e2eqVD  33707  ax6e2ndeqVD  33709  2uasbanhVD  33711  ax6e2ndeqALT  33731  bnj1533  33910  bnj983  34009  pm4.81ALT  34136  bj-dfbi6  34156  bj-consensus  34163  bj-falor2  34174  bj-bibibi  34175  bj-andnotim  34177  bj-cbvexw  34235  bj-cbvalv  34296  bj-equsexv  34312  bj-equsexvv  34313  bj-equs45fv  34331  bj-sb6  34350  bj-axext4  34355  bj-cleqh  34358  bj-hbaeb2  34391  bj-hbnaeb  34393  bj-equsal  34399  bj-dfcleq  34466  bj-csbsnlem  34470  bj-snsetex  34521  bj-snglex  34531  bj-1uplth  34565  bj-1uplex  34566  bj-2uplth  34579  bj-2uplex  34580  bj-elid  34599  bj-elid3  34601  bj-eldiag2  34607  isltrn2N  35844  rp-fakeimass  37736  rp-fakeanorass  37737  rp-fakenanass  37739  rp-isfinite4  37742  rp-isfinite5  37743  rp-isfinite6  37744  cnvtrrel  37782  cotr2g  37786  rp-imass  37795  frege54cor0a  37890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185