Theorem impbii 212

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicom  225  biid  264  2th  267  pm5.74  273  bitri  278  notnotb  318  con34b  319  notbi  322  bibi2i  340  con1b  361  con2b  362  bi2.04  392  imdi  394  pm4.8  398  pm4.81  399  impexp  456  ancom  466  anass  474  jcab  527  abab  840  impimprbi  842  orcom  884  dfor2  915  oridm  918  orbi2i  926  or12  934  pm4.72  964  oibabs  966  jaob  976  pm4.44  1012  pm4.79  1021  andi  1025  pm4.82  1041  cases2ALT  1064  consensus  1068  3impexp  1377  nanass  1540  tbw-bijust  1731  tbw-negdf  1732  19.26  1903  19.35  1910  19.21v  1972  19.23v  1975  19.41v  1982  19.3v  2015  19.9v  2017  equcom  2051  cbvalw  2068  alcomw  2078  excomw  2079  exexw  2086  sbbii  2113  sban  2117  sbv  2125  sbrimvw  2128  alcom  2196  19.3  2238  19.41  2271  sbalex  2278  equsexv  2302  sbim  2336  cbvalv1  2370  cbval  2427  equsex  2447  aecom  2456  equs45f  2488  dfsb1  2510  dfsb2  2522  sb6f  2526  dfmoeu  2560  moabs  2568  mo3  2589  mo4  2591  exmoeu  2606  moanimlem  2643  euan  2646  euanv  2649  2mo  2673  2eu6  2681  euae  2684  axextb  2735  eqcom  2767  nebi  3035  r19.35  3120  r19.26  3122  r19.21v  3187  gencbvex  3506  gencbvex2  3507  pm13.183  3620  rr19.3v  3621  rr19.28v  3622  euxfr2w  3678  euxfr2  3680  reu6  3684  reu3  3685  reuan  3844  dfss2  3917  sspss  4050  complss  4098  unineq  4234  uneqin  4235  difrab  4264  un00  4357  vvin  4359  sbnfc2  4397  ssdifeq0  4442  r19.2zb  4456  ralidmw  4472  ralidm  4473  pwidb  4579  snidb  4622  rabsnifsb  4683  tppreqb  4768  difsnb  4769  pwpw0  4774  sssn  4787  preq12b  4810  unissint  4932  uniintsn  4945  iununi  5059  al0ssb  5265  intex  5308  intnex  5309  axpweq  5315  iin0  5327  nfcvb  5341  eusvnfb  5358  eusv2nf  5360  ralxfrALT  5380  sspwb  5424  unipw  5425  opnz  5449  opth  5452  sbcop1  5464  opeqsng  5480  propeqop  5484  opthwiener  5491  opthhausdorff  5494  opthhausdorff0  5495  rexopabb  5506  ssopab2bw  5526  ssopab2b  5528  pwssun  5547  opelxp  5691  opthprc  5719  relsnb  5783  relop  5830  issetid  5834  xpid11  5916  elinxp  6012  eldmeldmressn  6018  iss  6031  iresn0n0  6050  asymref2  6111  xpnz  6151  xpdifid  6160  xpdifcnvepel  6161  ssrnres  6171  dfrel2  6182  relcnvtrg  6263  resssxp  6267  relrelss  6270  unixp0  6281  reuop  6291  dfpo2  6294  fn0  6663  funssxp  6731  f00  6757  f0bi  6758  dffo2  6793  f1o00  6853  fo00  6854  fv3  6896  dffn5  6936  dff2  7092  dff3  7093  dffo4  7096  dffo5  7097  exfo  7098  fmpt  7103  fompt  7111  ffnfv  7112  fsn  7129  fsn2  7130  funop  7146  funsneqopb  7149  fnsnbOLD  7164  isores1  7335  ssoprab2b  7482  eqoprab2bw  7483  eqfnov2  7543  unexb  7748  uniexb  7763  pwexb  7765  iunpw  7770  ordeleqon  7781  dford5  7783  onintrab  7795  ordsuc  7810  unon  7827  onuninsuci  7836  ordzsl  7841  onzsl  7842  f1oexbi  7925  ffoss  7943  1st2ndb  8026  frxp3  8149  suppssov1  8195  suppssov2  8196  suppssfv  8200  reldmtpos  8232  dfrecs3  8361  omopthi  8649  brinxper  8726  ecopover  8821  fsetexb  8865  mapsncnv  8900  mptelixpg  8942  elixpsn  8944  ixpsnf1o  8945  bren2  8989  en0  9024  en0ALT  9025  en0r  9026  en1  9030  en1b  9031  sbthb  9096  dom0  9103  canth2  9128  onfin2  9211  sdom1  9220  1sdom2dom  9224  fineqv  9237  unfilem1  9275  unfib  9279  pwfir  9286  pwfi  9288  fiint  9296  residfi  9305  unifpw  9322  wofib  9517  sucprcreg  9578  sucprcregOLD  9579  opthreg  9597  suc11reg  9598  infeq5  9616  rankwflemb  9775  r1elss  9788  pwwf  9789  unwf  9792  uniwf  9801  rankonid  9811  rankr1id  9844  rankuni  9845  rankxplim3  9863  scott0b  9876  scott0OLD  9877  karden  9898  kardenOLD  9899  djuexb  9914  isnum3  9959  oncard  9965  card1  9973  cardlim  9977  cardmin2  10004  pm54.43lem  10005  ween  10038  acnnum  10055  alephsuc2  10083  alephgeom  10085  iscard3  10096  dfac3  10124  dfac4  10125  dfac5lem3  10128  dfac5  10131  dfac2  10134  dfac8  10138  dfac9  10139  dfacacn  10144  dfac13  10145  dfac12r  10149  dfac12k  10150  kmlem2  10154  kmlem13  10165  djuinf  10191  ackbij2  10244  cflim2  10265  isfin4-2  10316  isfin4p1  10317  isf33lem  10368  compsscnv  10373  fin1a2lem6  10407  domtriom  10445  ac9  10485  ac9s  10495  fodomb  10529  brdom3  10531  brdom5  10532  brdom4  10533  brdom7disj  10534  brdom6disj  10535  iunfo  10547  sdomsdomcard  10568  gch2  10684  gch3  10685  eltsk2g  10760  grutsk  10831  ordpipq  10951  ltbtwnnq  10987  mappsrpr  11117  map2psrpr  11119  elreal2  11141  le2tri3i  11364  elnn0nn  12570  elnnnn0b  12572  elnnnn0c  12573  elnnz  12625  elnn0z  12628  elz2  12633  elnnz1  12644  0nn0m1nnn0  12675  eluz2b2  12970  elnn1uz2  12974  elpqb  13026  elioo4g  13459  eluzfz2b  13587  fzn0  13592  elfz1end  13609  fzass4  13617  elfz1b  13648  nn0fz0  13680  fzolb  13721  fzon0  13733  elfzo0  13756  elfzo0z  13757  elfzo1  13768  fzo1fzo0n0  13771  om2uzrani  14016  nn0opthi  14334  hashkf  14396  isfinite4  14426  hashprb  14461  hashf1  14522  elss2prb  14553  iswrdb  14585  wrdexb  14590  0wrd0  14605  s3rex  15021  wrdl3s3  15035  cotr2g  15049  trclun  15087  rexanuz  15433  rexuz3  15436  fsum0diag  15863  fprod0diag  16073  divalgmod  16496  sadcp1  16545  isprm6  16805  nnoddn2prmb  16905  4sqlem4  17044  fnpr2ob  17644  mreunirn  17685  isdrs2  18394  isacs5  18636  isacs4  18637  isacs3  18638  dfgrp2  19086  dfgrp3  19162  dfgrp3e  19163  isnsg3  19283  gicer  19404  oppgmndb  19482  oppggrpb  19485  pmtrfb  19592  invghm  19960  isringrng  20428  dfring2  20429  opprrngb  20487  opprringb  20489  ricer  20667  isnzr2hash  20680  isdomn4  20877  abvn0b  21002  gzrngunit  21646  dvdsrzring  21674  zringunit  21679  zlmlmod  21735  cygth  21784  frgpcyg  21786  zlmassa  22118  toprntopon  23150  tgclb  23195  iscldtop  23320  isnrm2  23583  isnrm3  23584  discmp  23623  dfconn2  23644  2ndcsb  23674  dis2ndc  23686  loclly  23713  unisngl  23753  locfindis  23756  iskgen2  23774  dfac14  23844  kqtop  23971  kqt0  23972  kqreg  23977  kqnrm  23978  hmpher  24010  hmphsymb  24012  hmph0  24021  kqhmph  24045  ist1-5lem  24046  elmptrab2  24054  isfil2  24082  filunirn  24108  isufil2  24134  hausflim  24207  isfcls  24235  alexsubALT  24277  istgp2  24317  ustbas  24453  xmetunirn  24563  dscmet  24798  dscopn  24799  isngp4  24838  zcld  25040  zlmclm  25340  iscmet2  25522  iundisj  25776  i1f1lem  25917  fta1b  26397  elply2  26421  elqaa  26554  aannenlem2  26565  wilth  27307  lgsne0  27571  2lgs  27643  2sqlem2  27654  ostth  27875  elno2  27890  bdayfo  27913  elons2  28523  eln0s2  28622  eln0s  28626  elzn0s  28663  eln0zs  28665  elnnzs  28666  remulscllem1  28765  mpteleeOLD  29352  wrdupgr  29542  wrdumgr  29554  umgrislfupgr  29580  lfuhgr3  29607  uspgrupgrushgr  29639  usgrumgruspgr  29642  usgruspgrb  29643  usgrislfuspgr  29647  uvtx01vtx  29857  pthspthcyc  30270  spthcycl  30271  wwlksnwwlksnon  30383  elwwlks2ons3  30423  clwwlkn1loopb  30513  eclclwwlkn1  30545  upgriseupth  30687  numclwwlkovh  30853  nmlno0lem  31274  isblo3i  31282  blocni  31286  hvsubeq0i  31544  hvaddcani  31546  bcseqi  31601  isch3  31722  norm1exi  31731  hhsssh  31750  shslubi  31866  dfch2  31888  pjoc1i  31912  pjchi  31913  shs00i  31931  chsscon3i  31942  chlejb1i  31957  chj00i  31968  shjshseli  31974  h1de2ctlem  32036  spanunsni  32060  cmcmi  32073  cmbr3i  32081  cmbr4i  32082  pj11i  32192  hosubeq0i  32307  dmadjrnb  32387  nmlnop0iALT  32476  lnopeq0i  32488  elunop2  32494  lnconi  32514  lncnopbd  32518  adjbdlnb  32565  adjbd1o  32566  adjeq0  32572  rnbra  32588  pjss1coi  32644  pjss2coi  32645  pjnormssi  32649  pjssdif2i  32655  pjssdif1i  32656  dfpjop  32663  pjinvari  32672  pjin2i  32674  pjci  32681  pjcmul1i  32682  pjcmul2i  32683  strb  32739  hstrbi  32747  mdsl1i  32802  atom1d  32834  chrelat2i  32846  cvbr4i  32848  cvexchi  32850  sumdmdi  32901  dmdbr4ati  32902  dmdbr5ati  32903  dmdbr6ati  32904  dmdbr7ati  32905  cdj3i  32922  eqtrb  32949  difeq  32993  iundisjf  33062  fpwrelmap  33204  iundisjfi  33267  xrge0tsmsbi  33514  dflring2  33903  dfufd2  33960  0mplrim  34024  ccfldextdgrr  34182  issgon  34633  measbasedom  34713  oddpwdc  34865  eulerpartlemt  34882  ballotlem2  35000  ballotlemrinv  35045  bnj1533  35361  bnj983  35460  r1omhf  35614  r1omhfb  35622  fineqvomonb  35645  fineqvnttrclse  35650  r1omhfbregs  35663  fineqvr1ombregs  35664  kardeq0  35682  karddom  35687  kardsdom  35688  kardexen  35689  satfv1  35942  satf0op  35956  fmla0xp  35962  fmla1  35966  elmsta  36127  antnestlaw1  36270  antnestlaw2  36271  antnestlaw3  36272  nepss  36297  dfon2  36369  distel  36380  fnimage  36506  altopthsn  36541  ellines  36732  rankeq1o  36751  opnrebl2  36940  df3nandALT1  37018  ttc00  37127  ttcwf  37143  ttcwf2  37144  ttcexbi  37152  ttc0el  37154  bj-animbi  37259  bj-dfbi6  37276  bj-consensus  37279  bj-falor2  37286  bj-bibibi  37287  bj-andnotim  37289  bj-alextruim  37367  bj-exextruan  37368  bj-ssbeq  37383  bj-19.41al  37389  bj-subst  37391  bj-eqs  37406  bj-cbvexw  37407  bj-sb  37420  bj-substax12  37457  bj-dfnnf3  37514  bj-equs45fv  37554  bj-hbaeb2  37561  bj-hbnaeb  37563  bj-equsal  37569  bj-sbsb  37580  bj-moeub  37592  bj-csbsnlem  37646  bj-snsetex  37707  bj-snglex  37717  bj-1uplth  37751  bj-1uplex  37752  bj-2uplth  37765  bj-2uplex  37766  bj-bm1.3ii  37808  bj-restpw  37842  bj-restuni  37847  bj-discrmoore  37861  bj-snmooreb  37864  bj-elid6  37922  bj-eldiag2  37929  mptsnunlem  38092  topdifinf  38103  elxp8  38125  finxp1o  38146  wl-moae  38279  wl-exeq  38297  wl-aleq  38298  wl-nfeqfb  38299  volsupnfl  38414  cover2  38465  isbnd3  38534  cntotbnd  38546  heibor  38571  isfld2  38755  isfldidl  38818  orfa  38832  eqbrb  38987  eqelb  38989  iss2  39092  issetssr  39331  n0el3  39484  detlem  39634  petlem  39663  eldisjs6  39688  prtlem16  39742  isltrn2N  40993  aks6d1c2p2  42985  aks6d1c6isolem3  43042  sn-iotalem  43091  dffltz  43480  eu6w  43522  3cubes  43535  ismrc  43546  isnacs3  43555  rexzrexnn0  43645  eldioph4b  43652  dford3  43869  wopprc  43871  ttac  43877  pw2f1ocnv  43878  dfac11  43903  dfac21  43907  isnumbasabl  43947  isnumbasgrp  43948  dfacbasgrp  43949  aaitgo  44003  dflim5  44170  nvocnvb  44262  dfno2  44268  ifpbi1b  44343  rp-fakeimass  44352  rp-fakeanorass  44353  rp-isfinite5  44357  rp-isfinite6  44358  dfsucon  44363  snen1g  44364  iscard4  44373  rtrclex  44457  cnvtrrel  44510  frege54cor0a  44703  isotone1  44888  isotone2  44889  gneispace  44974  k0004lem3  44989  grumnueq  45111  ismnushort  45125  nanorxor  45129  nzss  45141  pm10.55  45193  pm11.57  45213  pm13.192  45234  pm13.194  45236  ipo0  45272  ifr0  45273  xpexb  45276  3impexpbicom  45303  com3rgbi  45337  pm2.43bgbi  45340  pm2.43cbi  45341  sb5ALT  45348  trsbc  45363  2pm13.193  45375  ax6e2ndeq  45382  2uasbanh  45384  eelT01  45533  eel0T1  45534  uunT1  45602  zfregs2VD  45663  equncomVD  45690  trsbcVD  45699  undif3VD  45704  2pm13.193VD  45725  ax6e2eqVD  45729  ax6e2ndeqVD  45731  2uasbanhVD  45733  ax6e2ndeqALT  45753  tcfr  45786  mptssid  46070  elfzfzo  46110  allbutfi  46222  uzn0bi  46287  dvnprodlem3  46776  elaa2  47062  sge00  47204  elhoi  47370  ovn0  47394  ovolval4lem2  47478  wrddin2  47716  chndin2  47721  chnrin2  47726  confun  47827  afvfv0bi  48040  ffnafv  48059  afv2ndefb  48112  dfatafv2rnb  48115  afv2fv0b  48154  prpair  48401  sbcpr  48421  fpprel2  48657  sbgoldbmb  48702  vopnbgrelself  48771  isgrtri  48859  stgr1  48877  mgm2mgm  49142  nnpw2pb  49517  0aryfvalel  49564  mo0sn  49744  resinsnlem  49797  homf0  49935  isoval2  49961  oppccicb  49977  oppcciceq  49978  funcf2lem2  50008  initc  50017  isinito2  50425  isinito3  50426  termc  50445  dftermc3  50457  elsetrecs  50626  elpg  50640