Theorem impbii 209

Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 208. (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		impbi 208	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bicom  222  biid  261  2th  264  pm5.74  270  bitri  275  notnotb  315  con34b  316  notbi  319  bibi2i  337  con1b  358  con2b  359  bi2.04  387  imdi  389  pm4.8  392  pm4.81  393  impexp  450  ancom  460  anass  468  jcab  517  impimprbi  828  orcom  870  dfor2  901  oridm  904  orbi2i  912  or12  920  biorfriOLD  940  pm4.72  951  oibabs  953  jaob  963  pm4.44  998  pm4.79  1005  andi  1009  pm4.82  1025  cases2ALT  1048  consensus  1052  3impexp  1359  3jaobOLD  1429  nanass  1510  tbw-bijust  1698  tbw-negdf  1699  19.26  1870  19.35  1877  19.21v  1939  19.23v  1942  19.41v  1949  19.3v  1981  19.9v  1983  equcom  2017  cbvalw  2034  alcomw  2044  exexw  2051  sbbii  2076  sban  2080  sbv  2088  alcom  2159  19.3  2202  19.41  2235  sbalex  2242  sbalexOLD  2243  equsexv  2268  sbim  2303  cbvalv1  2342  cbval  2402  equsex  2422  aecom  2431  equs45f  2463  dfsb1  2485  dfsb2  2497  sb6f  2501  dfmoeu  2535  moabs  2542  mobii  2547  mo3  2563  mo4  2565  exmoeu  2580  moanimlem  2617  euan  2620  euanv  2623  2mo  2647  2eu6  2656  euae  2659  axextb  2710  eqcom  2742  nebi  3012  ralcom3OLD  3087  r19.35  3095  r19.35OLD  3096  r19.26  3098  r19.21v  3165  ceqsexOLD  3510  gencbvex  3520  gencbvex2  3521  pm13.183  3645  rr19.3v  3646  rr19.28v  3647  euxfr2w  3703  euxfr2  3705  reu6  3709  reu3  3710  reuan  3871  dfss2  3944  sspss  4077  complss  4126  unineq  4263  uneqin  4264  difrab  4293  ab0w  4354  sbnfc2  4414  un00  4420  disj  4425  ssdifeq0  4462  r19.2zb  4471  ralidmw  4483  ralidm  4487  ralf0  4489  pwidb  4596  snidb  4637  rabsnifsb  4698  tppreqb  4781  difsnb  4782  pwpw0  4789  sssn  4802  preq12b  4826  unissint  4948  uniintsn  4961  iununi  5075  al0ssb  5278  intex  5314  intnex  5315  axpweq  5321  iin0  5332  nfcvb  5346  eusvnfb  5363  eusv2nf  5365  ralxfrALT  5385  sspwb  5424  unipw  5425  opnz  5448  opth  5451  sbcop1  5463  opeqsng  5478  propeqop  5482  opthwiener  5489  opthhausdorff  5492  opthhausdorff0  5493  rexopabb  5503  ssopab2bw  5522  ssopab2b  5524  pwssun  5545  opelxp  5690  opthprc  5718  relsnb  5781  relop  5830  issetid  5834  xpid11  5912  elinxp  6006  eldmeldmressn  6012  iss  6022  iresn0n0  6041  asymref2  6106  xpnz  6148  xpdifid  6157  ssrnres  6167  dfrel2  6178  resssxp  6259  relrelss  6262  unixp0  6272  reuop  6282  dfpo2  6285  fn0  6668  funssxp  6733  f00  6759  f0bi  6760  dffo2  6793  f1o00  6852  fo00  6853  fv3  6893  dffn5  6936  dff2  7088  dff3  7089  dffo4  7092  dffo5  7093  exfo  7094  fmpt  7099  fompt  7107  ffnfv  7108  fsn  7124  fsn2  7125  funop  7138  funsneqopb  7141  fnsnbOLD  7157  isores1  7326  ssoprab2b  7474  eqoprab2bw  7475  eqfnov2  7535  unexb  7739  unexbOLD  7740  uniexb  7756  pwexb  7758  iunpw  7763  ordeleqon  7774  dford5  7776  onintrab  7788  ordsuc  7805  unon  7823  onuninsuci  7833  ordzsl  7838  onzsl  7839  f1oexbi  7922  ffoss  7942  1st2ndb  8026  frxp3  8148  suppssov1  8194  suppssov2  8195  suppssfv  8199  reldmtpos  8231  dfrecs3  8384  dfrecs3OLD  8385  omopthi  8671  brinxper  8746  ecopover  8833  fsetexb  8876  mapsncnv  8905  mptelixpg  8947  elixpsn  8949  ixpsnf1o  8950  bren2  8995  en0  9030  en0ALT  9031  en0r  9032  en1  9036  en1b  9037  sbthb  9106  dom0  9114  canth2  9142  onfin2  9238  sdom1  9248  sdom1OLD  9249  1sdom2dom  9253  1sdomOLD  9255  fineqv  9269  unfilem1  9313  unfib  9317  pwfir  9325  pwfi  9327  fiint  9336  fiintOLD  9337  residfi  9348  unifpw  9365  wofib  9557  sucprcreg  9613  opthreg  9630  suc11reg  9631  infeq5  9649  rankwflemb  9805  r1elss  9818  pwwf  9819  unwf  9822  uniwf  9831  rankonid  9841  rankr1id  9874  rankuni  9875  rankxplim3  9893  scott0  9898  karden  9907  djuexb  9921  isnum3  9966  oncard  9972  card1  9980  cardlim  9984  cardmin2  10011  pm54.43lem  10012  ween  10047  acnnum  10064  alephsuc2  10092  alephgeom  10094  iscard3  10105  dfac3  10133  dfac4  10134  dfac5lem3  10137  dfac5  10141  dfac2  10144  dfac8  10148  dfac9  10149  dfacacn  10154  dfac13  10155  dfac12r  10159  dfac12k  10160  kmlem2  10164  kmlem13  10175  djuinf  10201  ackbij2  10254  cflim2  10275  isfin4-2  10326  isfin4p1  10327  isf33lem  10378  compsscnv  10383  fin1a2lem6  10417  domtriom  10455  ac9  10495  ac9s  10505  fodomb  10538  brdom3  10540  brdom5  10541  brdom4  10542  brdom7disj  10543  brdom6disj  10544  iunfo  10551  sdomsdomcard  10572  gch2  10687  gch3  10688  eltsk2g  10763  grutsk  10834  ordpipq  10954  ltbtwnnq  10990  mappsrpr  11120  map2psrpr  11122  elreal2  11144  le2tri3i  11363  elnn0nn  12541  elnnnn0b  12543  elnnnn0c  12544  elnnz  12596  elnn0z  12599  elz2  12604  elnnz1  12616  eluz2b2  12935  elnn1uz2  12939  elpqb  12990  elioo4g  13421  eluzfz2b  13548  fzn0  13553  elfz1end  13569  fzass4  13577  elfz1b  13608  nn0fz0  13640  fzolb  13680  fzon0  13692  elfzo0  13715  elfzo0z  13716  elfzo1  13727  fzo1fzo0n0  13729  om2uzrani  13968  nn0opthi  14286  hashkf  14348  isfinite4  14378  hashprb  14413  hashf1  14473  elss2prb  14504  iswrdb  14536  wrdexb  14541  0wrd0  14556  wrdl3s3  14979  cotr2g  14993  trclun  15031  rexanuz  15362  rexuz3  15365  fsum0diag  15791  fprod0diag  16000  divalgmod  16423  sadcp1  16472  isprm6  16731  nnoddn2prmb  16831  4sqlem4  16970  fnpr2ob  17570  mreunirn  17611  isdrs2  18316  isacs5  18556  isacs4  18557  isacs3  18558  dfgrp2  18943  dfgrp3  19020  dfgrp3e  19021  isnsg3  19141  gicer  19258  oppgmndb  19336  oppggrpb  19339  pmtrfb  19444  invghm  19812  isringrng  20245  opprrngb  20304  opprringb  20306  isnzr2hash  20477  isdomn4  20674  abvn0b  20794  gzrngunit  21399  dvdsrzring  21420  zringunit  21425  zlmlmod  21481  cygth  21530  frgpcyg  21532  zlmassa  21861  toprntopon  22861  tgclb  22906  iscldtop  23031  isnrm2  23294  isnrm3  23295  discmp  23334  dfconn2  23355  2ndcsb  23385  dis2ndc  23396  loclly  23423  unisngl  23463  locfindis  23466  iskgen2  23484  dfac14  23554  kqtop  23681  kqt0  23682  kqreg  23687  kqnrm  23688  hmpher  23720  hmphsymb  23722  hmph0  23731  kqhmph  23755  ist1-5lem  23756  elmptrab2  23764  isfil2  23792  filunirn  23818  isufil2  23844  hausflim  23917  isfcls  23945  alexsubALT  23987  istgp2  24027  ustbas  24164  xmetunirn  24274  dscmet  24509  dscopn  24510  isngp4  24549  zcld  24751  zlmclm  25061  iscmet2  25244  iundisj  25499  i1f1lem  25640  fta1b  26127  elply2  26151  elqaa  26280  aannenlem2  26287  wilth  27031  lgsne0  27296  2lgs  27368  2sqlem2  27379  ostth  27600  elno2  27616  bdayfo  27639  elons2  28198  eln0s  28275  elzn0s  28301  eln0zs  28303  elnnzs  28304  remulscllem1  28349  mptelee  28820  wrdupgr  29010  wrdumgr  29022  umgrislfupgr  29048  uspgrupgrushgr  29104  usgrumgruspgr  29107  usgruspgrb  29108  usgrislfuspgr  29112  uvtx01vtx  29322  pthspthcyc  29731  wwlksnwwlksnon  29843  elwwlks2ons3  29883  clwwlkn1loopb  29970  eclclwwlkn1  30002  upgriseupth  30134  numclwwlkovh  30300  nmlno0lem  30720  isblo3i  30728  blocni  30732  hvsubeq0i  30990  hvaddcani  30992  bcseqi  31047  isch3  31168  norm1exi  31177  hhsssh  31196  shslubi  31312  dfch2  31334  pjoc1i  31358  pjchi  31359  shs00i  31377  chsscon3i  31388  chlejb1i  31403  chj00i  31414  shjshseli  31420  h1de2ctlem  31482  spanunsni  31506  cmcmi  31519  cmbr3i  31527  cmbr4i  31528  pj11i  31638  hosubeq0i  31753  dmadjrnb  31833  nmlnop0iALT  31922  lnopeq0i  31934  elunop2  31940  lnconi  31960  lncnopbd  31964  adjbdlnb  32011  adjbd1o  32012  adjeq0  32018  rnbra  32034  pjss1coi  32090  pjss2coi  32091  pjnormssi  32095  pjssdif2i  32101  pjssdif1i  32102  dfpjop  32109  pjinvari  32118  pjin2i  32120  pjci  32127  pjcmul1i  32128  pjcmul2i  32129  strb  32185  hstrbi  32193  mdsl1i  32248  atom1d  32280  chrelat2i  32292  cvbr4i  32294  cvexchi  32296  sumdmdi  32347  dmdbr4ati  32348  dmdbr5ati  32349  dmdbr6ati  32350  dmdbr7ati  32351  cdj3i  32368  eqtrb  32401  difeq  32445  iundisjf  32516  fpwrelmap  32656  iundisjfi  32719  xrge0tsmsbi  33003  dfufd2  33511  ccfldextdgrr  33659  issgon  34100  measbasedom  34179  oddpwdc  34332  eulerpartlemt  34349  ballotlem2  34467  ballotlemrinv  34512  bnj1533  34829  bnj983  34928  0nn0m1nnn0  35081  lfuhgr3  35088  spthcycl  35097  satfv1  35331  satf0op  35345  fmla0xp  35351  fmla1  35355  elmsta  35516  nepss  35681  dfon2  35756  distel  35767  fnimage  35893  altopthsn  35925  ellines  36116  rankeq1o  36135  opnrebl2  36285  df3nandALT1  36363  bj-animbi  36523  bj-dfbi6  36539  bj-consensus  36542  bj-falor2  36549  bj-bibibi  36550  bj-andnotim  36552  bj-cbval  36613  bj-cbvex  36614  bj-ssbeq  36617  bj-19.41al  36623  bj-subst  36625  bj-eqs  36639  bj-cbvexw  36640  bj-sb  36651  bj-substax12  36685  bj-dfnnf3  36721  bj-equs45fv  36775  bj-hbaeb2  36782  bj-hbnaeb  36784  bj-equsal  36790  bj-sbsb  36801  bj-moeub  36813  bj-csbsnlem  36867  bj-snsetex  36927  bj-snglex  36937  bj-1uplth  36971  bj-1uplex  36972  bj-2uplth  36985  bj-2uplex  36986  bj-bm1.3ii  37028  bj-restpw  37056  bj-restuni  37061  bj-discrmoore  37075  bj-snmooreb  37078  bj-elid6  37134  bj-eldiag2  37141  mptsnunlem  37302  topdifinf  37313  elxp8  37335  finxp1o  37356  wl-moae  37480  wl-exeq  37498  wl-aleq  37499  wl-nfeqfb  37500  wl-ax11-lem6  37554  volsupnfl  37635  cover2  37685  isbnd3  37754  cntotbnd  37766  heibor  37791  isfld2  37975  isfldidl  38038  orfa  38052  eqbrb  38197  eqelb  38199  iss2  38308  issetssr  38467  n0el3  38615  detlem  38747  petlem  38776  prtlem16  38833  isltrn2N  40085  aks6d1c2p2  42078  aks6d1c6isolem3  42135  sn-iotalem  42218  dffltz  42604  eu6w  42646  3cubes  42660  ismrc  42671  isnacs3  42680  rexzrexnn0  42774  eldioph4b  42781  dford3  42999  wopprc  43001  ttac  43007  pw2f1ocnv  43008  dfac11  43033  dfac21  43037  isnumbasabl  43077  isnumbasgrp  43078  dfacbasgrp  43079  aaitgo  43133  dflim5  43300  nvocnvb  43393  dfno2  43399  ifpbi1b  43474  rp-fakeimass  43483  rp-fakeanorass  43484  rp-isfinite5  43488  rp-isfinite6  43489  dfsucon  43494  snen1g  43495  iscard4  43504  rtrclex  43588  cnvtrrel  43641  frege54cor0a  43834  isotone1  44019  isotone2  44020  gneispace  44105  k0004lem3  44120  grumnueq  44259  ismnushort  44273  nanorxor  44277  nzss  44289  pm10.55  44341  pm11.57  44361  pm13.192  44382  pm13.194  44384  ipo0  44421  ifr0  44422  xpexb  44426  3impexpbicom  44453  com3rgbi  44487  pm2.43bgbi  44490  pm2.43cbi  44491  sb5ALT  44498  trsbc  44513  2pm13.193  44525  ax6e2ndeq  44532  2uasbanh  44534  eelT01  44683  eel0T1  44684  uunT1  44752  zfregs2VD  44813  equncomVD  44840  trsbcVD  44849  undif3VD  44854  2pm13.193VD  44875  ax6e2eqVD  44879  ax6e2ndeqVD  44881  2uasbanhVD  44883  ax6e2ndeqALT  44903  tcfr  44936  mptssid  45213  elfzfzo  45253  allbutfi  45368  uzn0bi  45434  dvnprodlem3  45925  elaa2  46211  sge00  46353  elhoi  46519  ovn0  46543  ovolval4lem2  46627  confun  46916  afvfv0bi  47129  ffnafv  47148  afv2ndefb  47201  dfatafv2rnb  47204  afv2fv0b  47243  prpair  47463  sbcpr  47483  fpprel2  47703  sbgoldbmb  47748  vopnbgrelself  47816  isgrtri  47903  stgr1  47921  mgm2mgm  48150  nnpw2pb  48515  0aryfvalel  48562  mo0sn  48742  resinsnlem  48794  homf0  48932  oppccicb  48966  oppcciceq  48967  funcf2lem2  48995  isinito2  49332  isinito3  49333  termc  49352  dftermc3  49364  elsetrecs  49512  elpg  49526