Theorem impbii 211

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bicom  224  biid  263  2th  266  pm5.74  272  bitri  277  notnotb  317  con34b  318  notbi  321  bibi2i  340  con1b  361  con2b  362  bi2.04  391  imdi  393  pm4.8  395  pm4.81  396  impexp  453  ancom  463  anass  471  jcab  520  impimprbi  826  orcom  866  dfor2  898  oridm  901  orbi2i  909  or12  917  biorfi  935  pm4.72  946  oibabs  948  jaob  958  pm4.44  993  pm4.79  1000  andi  1004  pm4.82  1020  cases2ALT  1043  consensus  1047  3impexp  1354  3jaob  1422  nanass  1500  norassOLD  1534  tbw-bijust  1699  tbw-negdf  1700  19.26  1871  19.35  1878  19.21v  1940  19.23v  1943  19.41v  1950  19.3v  1986  19.9v  1988  equcom  2025  cbvalw  2042  sbbii  2081  sban  2086  sbv  2098  alcom  2163  19.3  2202  19.41  2237  sb6OLD  2280  sbbibOLD  2289  sbim  2311  sbimvOLD  2325  cbvalv1  2361  cbval  2416  cbvalvOLD  2420  equsex  2440  aecom  2449  equs45f  2482  dfsb1  2510  dfsb2  2532  sb6f  2537  sbbiiALT  2578  sb6ALT  2585  dfsb2ALT  2591  sb6fALT  2602  sbimALT  2608  dfmoeu  2618  moabs  2625  mobii  2631  mo3  2648  mo4  2650  exmoeu  2666  moanimlem  2703  euan  2706  euanv  2709  2mo  2733  2eu6  2742  euae  2745  axextb  2796  eqcom  2828  nebi  3096  r19.26  3170  r19.35  3341  ralcom3  3364  ceqsex  3540  gencbvex  3549  gencbvex2  3550  clel5OLD  3658  pm13.183  3659  pm13.183OLD  3660  rr19.3v  3661  rr19.28v  3662  euxfr2w  3711  euxfr2  3713  reu6  3717  reu3  3718  reuan  3880  sspss  4076  complss  4123  unineq  4254  uneqin  4255  difrab  4277  sbnfc2  4388  un00  4394  ssdifeq0  4432  r19.2zb  4441  pwidb  4562  snidb  4600  rabsnifsb  4658  tppreqb  4738  difsnb  4739  pwpw0  4746  sssn  4759  preq12b  4781  pwsnOLD  4831  unissint  4900  uniintsn  4913  iununi  5021  al0ssb  5212  intex  5240  intnex  5241  iin0  5261  axpweq  5265  nfcvb  5277  eusvnfb  5294  eusv2nf  5296  ralxfrALT  5316  sspwb  5342  unipw  5343  opnz  5365  opth  5368  sbcop1  5379  opeqsng  5393  propeqop  5397  opthwiener  5404  opthhausdorff  5407  opthhausdorff0  5408  rexopabb  5415  ssopab2bw  5434  ssopab2b  5436  pwssun  5456  opelxp  5591  opthprc  5616  relsnb  5675  relop  5721  issetid  5725  xpid11  5802  elinxp  5890  eldmeldmressn  5896  iss  5903  iresn0n0  5923  asymref2  5977  xpnz  6016  xpdifid  6025  ssrnres  6035  dfrel2  6046  relrelss  6124  unixp0  6134  reuop  6144  fn0  6479  funssxp  6535  f00  6561  f0bi  6562  dffo2  6594  f1o00  6649  fo00  6650  fv3  6688  dffn5  6724  dff2  6865  dff3  6866  dffo4  6869  dffo5  6870  exfo  6871  fmpt  6874  ffnfv  6882  fsn  6897  fsn2  6898  funop  6911  funsneqopb  6914  fnsnb  6928  isores1  7087  ssoprab2b  7223  eqoprab2bw  7224  eqfnov2  7281  unexb  7471  uniexb  7486  pwexb  7488  iunpw  7493  ordeleqon  7503  onintrab  7516  unon  7546  onuninsuci  7555  ordzsl  7560  onzsl  7561  f1oexbi  7633  ffoss  7647  1st2ndb  7729  suppssov1  7862  suppssfv  7866  reldmtpos  7900  dfrecs3  8009  omopthi  8284  ecopover  8401  mapsncnv  8457  mptelixpg  8499  elixpsn  8501  ixpsnf1o  8502  bren2  8540  en0  8572  en1  8576  en1b  8577  sbthb  8638  canth2  8670  onfin2  8710  sdom1  8718  1sdom  8721  fineqv  8733  unfilem1  8782  fiint  8795  residfi  8805  pwfi  8819  unifpw  8827  wofib  9009  sucprcreg  9065  opthreg  9081  suc11reg  9082  infeq5  9100  rankwflemb  9222  r1elss  9235  pwwf  9236  unwf  9239  uniwf  9248  rankonid  9258  rankr1id  9291  rankuni  9292  rankxplim3  9310  scott0  9315  karden  9324  djuexb  9338  isnum3  9383  oncard  9389  card1  9397  cardlim  9401  cardmin2  9427  pm54.43lem  9428  ween  9461  acnnum  9478  alephsuc2  9506  alephgeom  9508  iscard3  9519  dfac3  9547  dfac4  9548  dfac5lem3  9551  dfac5  9554  dfac2  9557  dfac8  9561  dfac9  9562  dfacacn  9567  dfac13  9568  dfac12r  9572  dfac12k  9573  kmlem2  9577  kmlem13  9588  djuinf  9614  ackbij2  9665  cflim2  9685  isfin4-2  9736  isfin4p1  9737  isf33lem  9788  compsscnv  9793  fin1a2lem6  9827  domtriom  9865  ac9  9905  ac9s  9915  fodomb  9948  brdom3  9950  brdom5  9951  brdom4  9952  brdom7disj  9953  brdom6disj  9954  iunfo  9961  sdomsdomcard  9982  gch2  10097  gch3  10098  eltsk2g  10173  grutsk  10244  ordpipq  10364  ltbtwnnq  10400  mappsrpr  10530  map2psrpr  10532  elreal2  10554  le2tri3i  10770  elnn0nn  11940  elnnnn0b  11942  elnnnn0c  11943  elnnz  11992  elnn0z  11995  elz2  12000  elnnz1  12009  eluz2b2  12322  elnn1uz2  12326  elpqb  12376  elioo4g  12798  eluzfz2b  12917  fzn0  12922  elfz1end  12938  fzass4  12946  elfz1b  12977  nn0fz0  13006  fzolb  13045  fzon0  13056  elfzo0  13079  elfzo0z  13080  elfzo1  13088  fzo1fzo0n0  13089  om2uzrani  13321  nn0opthi  13631  hashkf  13693  isfinite4  13724  hashprb  13759  hashf1  13816  elss2prb  13846  iswrdb  13868  wrdexb  13874  0wrd0  13890  wrdl3s3  14326  cotr2g  14336  trclun  14374  sqr0lem  14600  rexanuz  14705  rexuz3  14708  fsum0diag  15132  fprod0diag  15340  divalgmod  15757  sadcp1  15804  isprm6  16058  nnoddn2prmb  16150  4sqlem4  16288  fnpr2ob  16831  mreunirn  16872  isdrs2  17549  isacs5  17782  isacs4  17783  isacs3  17784  dfgrp2  18128  dfgrp3  18198  dfgrp3e  18199  isnsg3  18312  gicer  18416  oppgmndb  18483  oppggrpb  18486  pmtrfb  18593  invghm  18954  opprringb  19382  isnzr2hash  20037  abvn0b  20075  gzrngunit  20611  dvdsrzring  20630  zringunit  20635  zlmlmod  20670  zlmassa  20671  cygth  20718  frgpcyg  20720  toprntopon  21533  tgclb  21578  iscldtop  21703  isnrm2  21966  isnrm3  21967  discmp  22006  dfconn2  22027  2ndcsb  22057  dis2ndc  22068  loclly  22095  unisngl  22135  locfindis  22138  iskgen2  22156  dfac14  22226  kqtop  22353  kqt0  22354  kqreg  22359  kqnrm  22360  hmpher  22392  hmphsymb  22394  hmph0  22403  kqhmph  22427  ist1-5lem  22428  elmptrab2  22436  isfil2  22464  filunirn  22490  isufil2  22516  hausflim  22589  isfcls  22617  alexsubALT  22659  istgp2  22699  ustbas  22836  xmetunirn  22947  dscmet  23182  dscopn  23183  isngp4  23221  zcld  23421  zlmclm  23716  iscmet2  23897  iundisj  24149  i1f1lem  24290  fta1b  24763  elply2  24786  elqaa  24911  aannenlem2  24918  wilth  25648  lgsne0  25911  2lgs  25983  2sqlem2  25994  ostth  26215  mptelee  26681  wrdupgr  26870  wrdumgr  26882  umgrislfupgr  26908  uspgrupgrushgr  26962  usgrumgruspgr  26965  usgruspgrb  26966  usgrislfuspgr  26969  uvtx01vtx  27179  wwlksnwwlksnon  27694  elwwlks2ons3  27734  clwwlkn1loopb  27821  eclclwwlkn1  27854  upgriseupth  27986  numclwwlkovh  28152  nmlno0lem  28570  isblo3i  28578  blocni  28582  hvsubeq0i  28840  hvaddcani  28842  bcseqi  28897  isch3  29018  norm1exi  29027  hhsssh  29046  shslubi  29162  dfch2  29184  pjoc1i  29208  pjchi  29209  shs00i  29227  chsscon3i  29238  chlejb1i  29253  chj00i  29264  shjshseli  29270  h1de2ctlem  29332  spanunsni  29356  cmcmi  29369  cmbr3i  29377  cmbr4i  29378  pj11i  29488  hosubeq0i  29603  dmadjrnb  29683  nmlnop0iALT  29772  lnopeq0i  29784  elunop2  29790  lnconi  29810  lncnopbd  29814  adjbdlnb  29861  adjbd1o  29862  adjeq0  29868  rnbra  29884  pjss1coi  29940  pjss2coi  29941  pjnormssi  29945  pjssdif2i  29951  pjssdif1i  29952  dfpjop  29959  pjinvari  29968  pjin2i  29970  pjci  29977  pjcmul1i  29978  pjcmul2i  29979  strb  30035  hstrbi  30043  mdsl1i  30098  atom1d  30130  chrelat2i  30142  cvbr4i  30144  cvexchi  30146  sumdmdi  30197  dmdbr4ati  30198  dmdbr5ati  30199  dmdbr6ati  30200  dmdbr7ati  30201  cdj3i  30218  eqtrb  30238  difeq  30280  iundisjf  30339  cnvoprabOLD  30456  fpwrelmap  30469  iundisjfi  30519  xrge0tsmsbi  30693  ccfldextdgrr  31057  issgon  31382  measbasedom  31461  oddpwdc  31612  eulerpartlemt  31629  ballotlem2  31746  ballotlemrinv  31791  bnj1533  32124  bnj983  32223  0nn0m1nnn0  32351  lfuhgr3  32366  spthcycl  32376  satfv1  32610  satf0op  32624  fmla0xp  32630  fmla1  32634  elmsta  32795  nepss  32948  dford5  32957  dfpo2  32991  dfon2  33037  distel  33048  elno2  33161  bdayfo  33182  fnimage  33390  altopthsn  33422  ellines  33613  rankeq1o  33632  opnrebl2  33669  df3nandALT1  33747  bj-animbi  33894  bj-dfbi6  33908  bj-consensus  33911  bj-falor2  33919  bj-bibibi  33920  bj-andnotim  33922  bj-cbval  33982  bj-cbvex  33983  bj-ssbeq  33986  bj-19.41al  33992  bj-sb56  33994  bj-eqs  34008  bj-cbvexw  34009  bj-sb  34021  bj-dfnnf3  34086  bj-equs45fv  34133  bj-hbaeb2  34141  bj-hbnaeb  34143  bj-equsal  34149  bj-sbsb  34160  bj-moeub  34173  bj-csbsnlem  34223  bj-snsetex  34278  bj-snglex  34288  bj-1uplth  34322  bj-1uplex  34323  bj-2uplth  34336  bj-2uplex  34337  bj-bm1.3ii  34360  bj-restpw  34386  bj-restuni  34391  bj-discrmoore  34406  bj-snmooreb  34409  bj-elid6  34465  bj-eldiag2  34472  mptsnunlem  34622  topdifinf  34633  elxp8  34655  finxp1o  34676  wl-moae  34771  wl-exeq  34789  wl-aleq  34790  wl-nfeqfb  34791  wl-ax11-lem6  34837  volsupnfl  34952  cover2  35004  isbnd3  35077  cntotbnd  35089  heibor  35114  isfld2  35298  isfldidl  35361  orfa  35375  eqelb  35517  iss2  35616  issetssr  35758  n0el3  35900  prtlem16  36020  isltrn2N  37271  dffltz  39320  3cubes  39336  ismrc  39347  isnacs3  39356  rexzrexnn0  39450  eldioph4b  39457  dford3  39674  wopprc  39676  ttac  39682  pw2f1ocnv  39683  dfac11  39711  dfac21  39715  isnumbasabl  39755  isnumbasgrp  39756  dfacbasgrp  39757  aaitgo  39811  ifpbi1b  39918  rp-fakeimass  39927  rp-fakeanorass  39928  rp-isfinite5  39932  rp-isfinite6  39933  dfsucon  39938  snen1g  39939  iscard4  39949  rtrclex  40026  cnvtrrel  40064  rp-imass  40166  frege54cor0a  40258  isotone1  40447  isotone2  40448  gneispace  40533  k0004lem3  40548  grumnueq  40672  nanorxor  40686  nzss  40698  pm10.55  40750  pm11.57  40770  pm13.192  40791  pm13.194  40793  ipo0  40830  ifr0  40831  xpexb  40835  3impexpbicom  40862  com3rgbi  40897  pm2.43bgbi  40900  pm2.43cbi  40901  sb5ALT  40908  trsbc  40923  2pm13.193  40935  ax6e2ndeq  40942  2uasbanh  40944  eelT01  41094  eel0T1  41095  uunT1  41163  zfregs2VD  41224  equncomVD  41251  trsbcVD  41260  undif3VD  41265  2pm13.193VD  41286  ax6e2eqVD  41290  ax6e2ndeqVD  41292  2uasbanhVD  41294  ax6e2ndeqALT  41314  fompt  41502  mptssid  41560  elfzfzo  41591  allbutfi  41714  uzn0bi  41784  dvnprodlem3  42282  elaa2  42568  sge00  42707  elhoi  42873  ovn0  42897  ovolval4lem2  42981  confun  43224  afvfv0bi  43400  ffnafv  43419  afv2ndefb  43472  dfatafv2rnb  43475  afv2fv0b  43514  dfich2OLD  43665  prpair  43712  sbcpr  43732  fpprel2  43955  sbgoldbmb  44000  mgm2mgm  44183  isringrng  44201  nnpw2pb  44696  elsetrecs  44851  elpg  44865