Theorem impbii 208

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bicom  221  biid  260  2th  263  pm5.74  269  bitri  274  notnotb  314  con34b  315  notbi  318  bibi2i  336  con1b  357  con2b  358  bi2.04  386  imdi  388  pm4.8  391  pm4.81  392  impexp  449  ancom  459  anass  467  jcab  516  impimprbi  827  orcom  868  dfor2  899  oridm  902  orbi2i  910  or12  918  biorfi  936  pm4.72  947  oibabs  949  jaob  959  pm4.44  994  pm4.79  1001  andi  1005  pm4.82  1021  cases2ALT  1046  consensus  1050  3impexp  1355  3jaobOLD  1424  nanass  1504  tbw-bijust  1693  tbw-negdf  1694  19.26  1866  19.35  1873  19.21v  1935  19.23v  1938  19.41v  1946  19.3v  1978  19.9v  1980  equcom  2014  cbvalw  2031  alcomw  2040  exexw  2047  sbbii  2072  sban  2076  sbv  2084  alcom  2149  19.3  2191  19.41  2224  sbalex  2231  equsexv  2255  sbim  2293  cbvalv1  2332  cbval  2392  equsex  2412  aecom  2421  equs45f  2453  dfsb1  2475  dfsb2  2487  sb6f  2491  dfmoeu  2525  moabs  2532  mobii  2537  mo3  2553  mo4  2555  exmoeu  2570  moanimlem  2607  euan  2610  euanv  2613  2mo  2637  2eu6  2646  euae  2649  axextb  2700  eqcom  2733  nebi  3011  ralcom3OLD  3088  r19.35  3098  r19.35OLD  3099  r19.26  3101  r19.21v  3170  ceqsexOLD  3515  ceqsexvOLD  3517  gencbvex  3527  gencbvex2  3528  pm13.183  3653  rr19.3v  3654  rr19.28v  3655  euxfr2w  3714  euxfr2  3716  reu6  3720  reu3  3721  reuan  3889  dfss2  3965  sspss  4098  complss  4146  unineq  4279  uneqin  4280  difrab  4310  ab0w  4378  sbnfc2  4441  un00  4447  disj  4452  ssdifeq0  4491  r19.2zb  4500  ralidmw  4512  ralidm  4516  ralf0  4518  pwidb  4628  snidb  4668  rabsnifsb  4731  tppreqb  4814  difsnb  4815  pwpw0  4822  sssn  4835  preq12b  4857  unissint  4980  uniintsn  4995  iununi  5107  al0ssb  5313  intex  5344  intnex  5345  axpweq  5354  iin0  5366  nfcvb  5380  eusvnfb  5397  eusv2nf  5399  ralxfrALT  5419  sspwb  5455  unipw  5456  opnz  5479  opth  5482  sbcop1  5494  opeqsng  5509  propeqop  5513  opthwiener  5520  opthhausdorff  5523  opthhausdorff0  5524  rexopabb  5534  ssopab2bw  5553  ssopab2b  5555  pwssun  5577  opelxp  5718  opthprc  5746  relsnb  5808  relop  5857  issetid  5861  xpid11  5938  elinxp  6028  eldmeldmressn  6034  iss  6044  iresn0n0  6063  asymref2  6129  xpnz  6170  xpdifid  6179  ssrnres  6189  dfrel2  6200  resssxp  6281  relrelss  6284  unixp0  6294  reuop  6304  dfpo2  6307  fn0  6692  funssxp  6757  f00  6784  f0bi  6785  dffo2  6819  f1o00  6878  fo00  6879  fv3  6919  dffn5  6961  dff2  7113  dff3  7114  dffo4  7117  dffo5  7118  exfo  7119  fmpt  7124  fompt  7132  ffnfv  7133  fsn  7149  fsn2  7150  funop  7163  funsneqopb  7166  fnsnb  7180  isores1  7346  ssoprab2b  7494  eqoprab2bw  7495  eqfnov2  7556  unexb  7756  uniexb  7772  pwexb  7774  iunpw  7779  ordeleqon  7790  dford5  7792  onintrab  7805  ordsuc  7822  unon  7840  onuninsuci  7850  ordzsl  7855  onzsl  7856  f1oexbi  7941  ffoss  7959  1st2ndb  8043  frxp3  8165  suppssov1  8212  suppssov2  8213  suppssfv  8217  reldmtpos  8249  dfrecs3  8402  dfrecs3OLD  8403  omopthi  8691  brinxper  8763  ecopover  8850  fsetexb  8893  mapsncnv  8922  mptelixpg  8964  elixpsn  8966  ixpsnf1o  8967  bren2  9014  en0  9049  en0OLD  9050  en0ALT  9051  en0r  9052  en1  9057  en1OLD  9058  en1b  9059  en1bOLD  9060  sbthb  9132  dom0  9140  canth2  9168  onfin2  9265  sdom1  9276  sdom1OLD  9277  1sdom2dom  9281  1sdomOLD  9283  fineqv  9297  unfilem1  9344  unfib  9349  pwfir  9357  pwfi  9359  fiint  9368  fiintOLD  9369  residfi  9380  pwfiOLD  9391  unifpw  9399  wofib  9588  sucprcreg  9644  opthreg  9661  suc11reg  9662  infeq5  9680  rankwflemb  9836  r1elss  9849  pwwf  9850  unwf  9853  uniwf  9862  rankonid  9872  rankr1id  9905  rankuni  9906  rankxplim3  9924  scott0  9929  karden  9938  djuexb  9952  isnum3  9997  oncard  10003  card1  10011  cardlim  10015  cardmin2  10042  pm54.43lem  10043  ween  10078  acnnum  10095  alephsuc2  10123  alephgeom  10125  iscard3  10136  dfac3  10164  dfac4  10165  dfac5lem3  10168  dfac5  10171  dfac2  10174  dfac8  10178  dfac9  10179  dfacacn  10184  dfac13  10185  dfac12r  10189  dfac12k  10190  kmlem2  10194  kmlem13  10205  djuinf  10231  ackbij2  10286  cflim2  10306  isfin4-2  10357  isfin4p1  10358  isf33lem  10409  compsscnv  10414  fin1a2lem6  10448  domtriom  10486  ac9  10526  ac9s  10536  fodomb  10569  brdom3  10571  brdom5  10572  brdom4  10573  brdom7disj  10574  brdom6disj  10575  iunfo  10582  sdomsdomcard  10603  gch2  10718  gch3  10719  eltsk2g  10794  grutsk  10865  ordpipq  10985  ltbtwnnq  11021  mappsrpr  11151  map2psrpr  11153  elreal2  11175  le2tri3i  11394  elnn0nn  12566  elnnnn0b  12568  elnnnn0c  12569  elnnz  12620  elnn0z  12623  elz2  12628  elnnz1  12640  eluz2b2  12957  elnn1uz2  12961  elpqb  13012  elioo4g  13438  eluzfz2b  13564  fzn0  13569  elfz1end  13585  fzass4  13593  elfz1b  13624  nn0fz0  13653  fzolb  13692  fzon0  13704  elfzo0  13727  elfzo0z  13728  elfzo1  13736  fzo1fzo0n0  13737  om2uzrani  13972  nn0opthi  14287  hashkf  14349  isfinite4  14379  hashprb  14414  hashf1  14476  elss2prb  14506  iswrdb  14528  wrdexb  14533  0wrd0  14548  wrdl3s3  14971  cotr2g  14981  trclun  15019  rexanuz  15350  rexuz3  15353  fsum0diag  15781  fprod0diag  15988  divalgmod  16408  sadcp1  16455  isprm6  16715  nnoddn2prmb  16815  4sqlem4  16954  fnpr2ob  17573  mreunirn  17614  isdrs2  18331  isacs5  18573  isacs4  18574  isacs3  18575  dfgrp2  18957  dfgrp3  19033  dfgrp3e  19034  isnsg3  19154  gicer  19271  oppgmndb  19352  oppggrpb  19355  pmtrfb  19463  invghm  19831  isringrng  20266  opprrngb  20328  opprringb  20330  isnzr2hash  20501  isdomn4  20694  abvn0b  20815  gzrngunit  21430  dvdsrzring  21451  zringunit  21456  zlmlmod  21516  cygth  21569  frgpcyg  21571  zlmassa  21900  toprntopon  22918  tgclb  22964  iscldtop  23090  isnrm2  23353  isnrm3  23354  discmp  23393  dfconn2  23414  2ndcsb  23444  dis2ndc  23455  loclly  23482  unisngl  23522  locfindis  23525  iskgen2  23543  dfac14  23613  kqtop  23740  kqt0  23741  kqreg  23746  kqnrm  23747  hmpher  23779  hmphsymb  23781  hmph0  23790  kqhmph  23814  ist1-5lem  23815  elmptrab2  23823  isfil2  23851  filunirn  23877  isufil2  23903  hausflim  23976  isfcls  24004  alexsubALT  24046  istgp2  24086  ustbas  24223  xmetunirn  24334  dscmet  24572  dscopn  24573  isngp4  24612  zcld  24820  zlmclm  25130  iscmet2  25313  iundisj  25568  i1f1lem  25709  fta1b  26199  elply2  26223  elqaa  26350  aannenlem2  26357  wilth  27099  lgsne0  27364  2lgs  27436  2sqlem2  27447  ostth  27668  elno2  27684  bdayfo  27707  elons2  28252  eln0s  28324  elzn0s  28342  remulscllem1  28351  mptelee  28829  wrdupgr  29021  wrdumgr  29033  umgrislfupgr  29059  uspgrupgrushgr  29115  usgrumgruspgr  29118  usgruspgrb  29119  usgrislfuspgr  29123  uvtx01vtx  29333  wwlksnwwlksnon  29849  elwwlks2ons3  29889  clwwlkn1loopb  29976  eclclwwlkn1  30008  upgriseupth  30140  numclwwlkovh  30306  nmlno0lem  30726  isblo3i  30734  blocni  30738  hvsubeq0i  30996  hvaddcani  30998  bcseqi  31053  isch3  31174  norm1exi  31183  hhsssh  31202  shslubi  31318  dfch2  31340  pjoc1i  31364  pjchi  31365  shs00i  31383  chsscon3i  31394  chlejb1i  31409  chj00i  31420  shjshseli  31426  h1de2ctlem  31488  spanunsni  31512  cmcmi  31525  cmbr3i  31533  cmbr4i  31534  pj11i  31644  hosubeq0i  31759  dmadjrnb  31839  nmlnop0iALT  31928  lnopeq0i  31940  elunop2  31946  lnconi  31966  lncnopbd  31970  adjbdlnb  32017  adjbd1o  32018  adjeq0  32024  rnbra  32040  pjss1coi  32096  pjss2coi  32097  pjnormssi  32101  pjssdif2i  32107  pjssdif1i  32108  dfpjop  32115  pjinvari  32124  pjin2i  32126  pjci  32133  pjcmul1i  32134  pjcmul2i  32135  strb  32191  hstrbi  32199  mdsl1i  32254  atom1d  32286  chrelat2i  32298  cvbr4i  32300  cvexchi  32302  sumdmdi  32353  dmdbr4ati  32354  dmdbr5ati  32355  dmdbr6ati  32356  dmdbr7ati  32357  cdj3i  32374  eqtrb  32402  difeq  32445  iundisjf  32509  cnvoprabOLD  32634  fpwrelmap  32647  iundisjfi  32698  xrge0tsmsbi  32927  dfufd2  33425  ccfldextdgrr  33558  issgon  33956  measbasedom  34035  oddpwdc  34188  eulerpartlemt  34205  ballotlem2  34322  ballotlemrinv  34367  bnj1533  34697  bnj983  34796  0nn0m1nnn0  34940  lfuhgr3  34947  spthcycl  34957  satfv1  35191  satf0op  35205  fmla0xp  35211  fmla1  35215  elmsta  35376  nepss  35540  dfon2  35616  distel  35627  fnimage  35753  altopthsn  35785  ellines  35976  rankeq1o  35995  opnrebl2  36033  df3nandALT1  36111  bj-animbi  36262  bj-dfbi6  36279  bj-consensus  36282  bj-falor2  36290  bj-bibibi  36291  bj-andnotim  36293  bj-cbval  36353  bj-cbvex  36354  bj-ssbeq  36357  bj-19.41al  36363  bj-subst  36365  bj-eqs  36379  bj-cbvexw  36380  bj-sb  36392  bj-substax12  36426  bj-dfnnf3  36462  bj-equs45fv  36516  bj-hbaeb2  36523  bj-hbnaeb  36525  bj-equsal  36531  bj-sbsb  36542  bj-moeub  36554  bj-csbsnlem  36609  bj-snsetex  36670  bj-snglex  36680  bj-1uplth  36714  bj-1uplex  36715  bj-2uplth  36728  bj-2uplex  36729  bj-bm1.3ii  36771  bj-restpw  36799  bj-restuni  36804  bj-discrmoore  36818  bj-snmooreb  36821  bj-elid6  36877  bj-eldiag2  36884  mptsnunlem  37045  topdifinf  37056  elxp8  37078  finxp1o  37099  wl-moae  37211  wl-exeq  37229  wl-aleq  37230  wl-nfeqfb  37231  wl-ax11-lem6  37285  volsupnfl  37366  cover2  37416  isbnd3  37485  cntotbnd  37497  heibor  37522  isfld2  37706  isfldidl  37769  orfa  37783  eqbrb  37930  eqelb  37932  iss2  38042  issetssr  38201  n0el3  38349  detlem  38481  petlem  38510  prtlem16  38567  isltrn2N  39819  aks6d1c2p2  41817  aks6d1c6isolem3  41874  sn-iotalem  41943  dffltz  42288  eu6w  42331  3cubes  42347  ismrc  42358  isnacs3  42367  rexzrexnn0  42461  eldioph4b  42468  dford3  42686  wopprc  42688  ttac  42694  pw2f1ocnv  42695  dfac11  42723  dfac21  42727  isnumbasabl  42767  isnumbasgrp  42768  dfacbasgrp  42769  aaitgo  42823  dflim5  42995  nvocnvb  43089  dfno2  43095  ifpbi1b  43170  rp-fakeimass  43179  rp-fakeanorass  43180  rp-isfinite5  43184  rp-isfinite6  43185  dfsucon  43190  snen1g  43191  iscard4  43200  rtrclex  43284  cnvtrrel  43337  frege54cor0a  43530  isotone1  43715  isotone2  43716  gneispace  43801  k0004lem3  43816  grumnueq  43961  ismnushort  43975  nanorxor  43979  nzss  43991  pm10.55  44043  pm11.57  44063  pm13.192  44084  pm13.194  44086  ipo0  44123  ifr0  44124  xpexb  44128  3impexpbicom  44155  com3rgbi  44190  pm2.43bgbi  44193  pm2.43cbi  44194  sb5ALT  44201  trsbc  44216  2pm13.193  44228  ax6e2ndeq  44235  2uasbanh  44237  eelT01  44387  eel0T1  44388  uunT1  44456  zfregs2VD  44517  equncomVD  44544  trsbcVD  44553  undif3VD  44558  2pm13.193VD  44579  ax6e2eqVD  44583  ax6e2ndeqVD  44585  2uasbanhVD  44587  ax6e2ndeqALT  44607  mptssid  44849  elfzfzo  44891  allbutfi  45008  uzn0bi  45074  dvnprodlem3  45569  elaa2  45855  sge00  45997  elhoi  46163  ovn0  46187  ovolval4lem2  46271  confun  46554  afvfv0bi  46765  ffnafv  46784  afv2ndefb  46837  dfatafv2rnb  46840  afv2fv0b  46879  prpair  47073  sbcpr  47093  fpprel2  47313  sbgoldbmb  47358  vopnbgrelself  47422  gricer  47472  mgm2mgm  47604  nnpw2pb  47975  0aryfvalel  48022  mo0sn  48201  elsetrecs  48446  elpg  48460