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  2798  eqcom  2830  nebi  3098  r19.26  3172  r19.35  3343  ralcom3  3366  ceqsex  3542  gencbvex  3551  gencbvex2  3552  clel5OLD  3660  pm13.183  3661  pm13.183OLD  3662  rr19.3v  3663  rr19.28v  3664  euxfr2w  3713  euxfr2  3715  reu6  3719  reu3  3720  reuan  3882  sspss  4078  complss  4125  unineq  4256  uneqin  4257  difrab  4279  sbnfc2  4390  un00  4396  ssdifeq0  4434  r19.2zb  4443  pwidb  4564  snidb  4602  rabsnifsb  4660  tppreqb  4740  difsnb  4741  pwpw0  4748  sssn  4761  preq12b  4783  pwsnOLD  4833  unissint  4902  uniintsn  4915  iununi  5023  al0ssb  5214  intex  5242  intnex  5243  iin0  5263  axpweq  5267  nfcvb  5279  eusvnfb  5296  eusv2nf  5298  ralxfrALT  5318  sspwb  5344  unipw  5345  opnz  5367  opth  5370  sbcop1  5381  opeqsng  5395  propeqop  5399  opthwiener  5406  opthhausdorff  5409  opthhausdorff0  5410  rexopabb  5417  ssopab2bw  5436  ssopab2b  5438  pwssun  5458  opelxp  5593  opthprc  5618  relsnb  5677  relop  5723  issetid  5727  xpid11  5804  elinxp  5892  eldmeldmressn  5898  iss  5905  iresn0n0  5925  asymref2  5979  xpnz  6018  xpdifid  6027  ssrnres  6037  dfrel2  6048  relrelss  6126  unixp0  6136  reuop  6146  fn0  6481  funssxp  6537  f00  6563  f0bi  6564  dffo2  6596  f1o00  6651  fo00  6652  fv3  6690  dffn5  6726  dff2  6867  dff3  6868  dffo4  6871  dffo5  6872  exfo  6873  fmpt  6876  ffnfv  6884  fsn  6899  fsn2  6900  funop  6913  funsneqopb  6916  fnsnb  6930  isores1  7089  ssoprab2b  7225  eqoprab2bw  7226  eqfnov2  7283  unexb  7473  uniexb  7488  pwexb  7490  iunpw  7495  ordeleqon  7505  onintrab  7518  unon  7548  onuninsuci  7557  ordzsl  7562  onzsl  7563  f1oexbi  7635  ffoss  7649  1st2ndb  7731  suppssov1  7864  suppssfv  7868  reldmtpos  7902  dfrecs3  8011  omopthi  8286  ecopover  8403  mapsncnv  8459  mptelixpg  8501  elixpsn  8503  ixpsnf1o  8504  bren2  8542  en0  8574  en1  8578  en1b  8579  sbthb  8640  canth2  8672  onfin2  8712  sdom1  8720  1sdom  8723  fineqv  8735  unfilem1  8784  fiint  8797  residfi  8807  pwfi  8821  unifpw  8829  wofib  9011  sucprcreg  9067  opthreg  9083  suc11reg  9084  infeq5  9102  rankwflemb  9224  r1elss  9237  pwwf  9238  unwf  9241  uniwf  9250  rankonid  9260  rankr1id  9293  rankuni  9294  rankxplim3  9312  scott0  9317  karden  9326  djuexb  9340  isnum3  9385  oncard  9391  card1  9399  cardlim  9403  cardmin2  9429  pm54.43lem  9430  ween  9463  acnnum  9480  alephsuc2  9508  alephgeom  9510  iscard3  9521  dfac3  9549  dfac4  9550  dfac5lem3  9553  dfac5  9556  dfac2  9559  dfac8  9563  dfac9  9564  dfacacn  9569  dfac13  9570  dfac12r  9574  dfac12k  9575  kmlem2  9579  kmlem13  9590  djuinf  9616  ackbij2  9667  cflim2  9687  isfin4-2  9738  isfin4p1  9739  isf33lem  9790  compsscnv  9795  fin1a2lem6  9829  domtriom  9867  ac9  9907  ac9s  9917  fodomb  9950  brdom3  9952  brdom5  9953  brdom4  9954  brdom7disj  9955  brdom6disj  9956  iunfo  9963  sdomsdomcard  9984  gch2  10099  gch3  10100  eltsk2g  10175  grutsk  10246  ordpipq  10366  ltbtwnnq  10402  mappsrpr  10532  map2psrpr  10534  elreal2  10556  le2tri3i  10772  elnn0nn  11942  elnnnn0b  11944  elnnnn0c  11945  elnnz  11994  elnn0z  11997  elz2  12002  elnnz1  12011  eluz2b2  12324  elnn1uz2  12328  elpqb  12378  elioo4g  12800  eluzfz2b  12919  fzn0  12924  elfz1end  12940  fzass4  12948  elfz1b  12979  nn0fz0  13008  fzolb  13047  fzon0  13058  elfzo0  13081  elfzo0z  13082  elfzo1  13090  fzo1fzo0n0  13091  om2uzrani  13323  nn0opthi  13633  hashkf  13695  isfinite4  13726  hashprb  13761  hashf1  13818  elss2prb  13848  iswrdb  13870  wrdexb  13876  0wrd0  13892  wrdl3s3  14328  cotr2g  14338  trclun  14376  sqr0lem  14602  rexanuz  14707  rexuz3  14710  fsum0diag  15134  fprod0diag  15342  divalgmod  15759  sadcp1  15806  isprm6  16060  nnoddn2prmb  16152  4sqlem4  16290  fnpr2ob  16833  mreunirn  16874  isdrs2  17551  isacs5  17784  isacs4  17785  isacs3  17786  dfgrp2  18130  dfgrp3  18200  dfgrp3e  18201  isnsg3  18314  gicer  18418  oppgmndb  18485  oppggrpb  18488  pmtrfb  18595  invghm  18956  opprringb  19384  isnzr2hash  20039  abvn0b  20077  gzrngunit  20613  dvdsrzring  20632  zringunit  20637  zlmlmod  20672  zlmassa  20673  cygth  20720  frgpcyg  20722  toprntopon  21535  tgclb  21580  iscldtop  21705  isnrm2  21968  isnrm3  21969  discmp  22008  dfconn2  22029  2ndcsb  22059  dis2ndc  22070  loclly  22097  unisngl  22137  locfindis  22140  iskgen2  22158  dfac14  22228  kqtop  22355  kqt0  22356  kqreg  22361  kqnrm  22362  hmpher  22394  hmphsymb  22396  hmph0  22405  kqhmph  22429  ist1-5lem  22430  elmptrab2  22438  isfil2  22466  filunirn  22492  isufil2  22518  hausflim  22591  isfcls  22619  alexsubALT  22661  istgp2  22701  ustbas  22838  xmetunirn  22949  dscmet  23184  dscopn  23185  isngp4  23223  zcld  23423  zlmclm  23718  iscmet2  23899  iundisj  24151  i1f1lem  24292  fta1b  24765  elply2  24788  elqaa  24913  aannenlem2  24920  wilth  25650  lgsne0  25913  2lgs  25985  2sqlem2  25996  ostth  26217  mptelee  26683  wrdupgr  26872  wrdumgr  26884  umgrislfupgr  26910  uspgrupgrushgr  26964  usgrumgruspgr  26967  usgruspgrb  26968  usgrislfuspgr  26971  uvtx01vtx  27181  wwlksnwwlksnon  27696  elwwlks2ons3  27736  clwwlkn1loopb  27823  eclclwwlkn1  27856  upgriseupth  27988  numclwwlkovh  28154  nmlno0lem  28572  isblo3i  28580  blocni  28584  hvsubeq0i  28842  hvaddcani  28844  bcseqi  28899  isch3  29020  norm1exi  29029  hhsssh  29048  shslubi  29164  dfch2  29186  pjoc1i  29210  pjchi  29211  shs00i  29229  chsscon3i  29240  chlejb1i  29255  chj00i  29266  shjshseli  29272  h1de2ctlem  29334  spanunsni  29358  cmcmi  29371  cmbr3i  29379  cmbr4i  29380  pj11i  29490  hosubeq0i  29605  dmadjrnb  29685  nmlnop0iALT  29774  lnopeq0i  29786  elunop2  29792  lnconi  29812  lncnopbd  29816  adjbdlnb  29863  adjbd1o  29864  adjeq0  29870  rnbra  29886  pjss1coi  29942  pjss2coi  29943  pjnormssi  29947  pjssdif2i  29953  pjssdif1i  29954  dfpjop  29961  pjinvari  29970  pjin2i  29972  pjci  29979  pjcmul1i  29980  pjcmul2i  29981  strb  30037  hstrbi  30045  mdsl1i  30100  atom1d  30132  chrelat2i  30144  cvbr4i  30146  cvexchi  30148  sumdmdi  30199  dmdbr4ati  30200  dmdbr5ati  30201  dmdbr6ati  30202  dmdbr7ati  30203  cdj3i  30220  eqtrb  30240  difeq  30282  iundisjf  30341  cnvoprabOLD  30458  fpwrelmap  30471  iundisjfi  30521  xrge0tsmsbi  30695  ccfldextdgrr  31059  issgon  31384  measbasedom  31463  oddpwdc  31614  eulerpartlemt  31631  ballotlem2  31748  ballotlemrinv  31793  bnj1533  32126  bnj983  32225  0nn0m1nnn0  32353  lfuhgr3  32368  spthcycl  32378  satfv1  32612  satf0op  32626  fmla0xp  32632  fmla1  32636  elmsta  32797  nepss  32950  dford5  32959  dfpo2  32993  dfon2  33039  distel  33050  elno2  33163  bdayfo  33184  fnimage  33392  altopthsn  33424  ellines  33615  rankeq1o  33634  opnrebl2  33671  df3nandALT1  33749  bj-animbi  33896  bj-dfbi6  33910  bj-consensus  33913  bj-falor2  33921  bj-bibibi  33922  bj-andnotim  33924  bj-cbval  33984  bj-cbvex  33985  bj-ssbeq  33988  bj-19.41al  33994  bj-sb56  33996  bj-eqs  34010  bj-cbvexw  34011  bj-sb  34023  bj-dfnnf3  34088  bj-equs45fv  34135  bj-hbaeb2  34143  bj-hbnaeb  34145  bj-equsal  34151  bj-sbsb  34162  bj-moeub  34175  bj-csbsnlem  34222  bj-snsetex  34277  bj-snglex  34287  bj-1uplth  34321  bj-1uplex  34322  bj-2uplth  34335  bj-2uplex  34336  bj-bm1.3ii  34359  bj-restpw  34385  bj-restuni  34390  bj-discrmoore  34405  bj-snmooreb  34408  bj-elid6  34464  bj-eldiag2  34471  mptsnunlem  34621  topdifinf  34632  elxp8  34654  finxp1o  34675  wl-moae  34758  wl-exeq  34776  wl-aleq  34777  wl-nfeqfb  34778  wl-ax11-lem6  34824  volsupnfl  34939  cover2  34991  isbnd3  35064  cntotbnd  35076  heibor  35101  isfld2  35285  isfldidl  35348  orfa  35362  eqelb  35504  iss2  35603  issetssr  35745  n0el3  35887  prtlem16  36007  isltrn2N  37258  dffltz  39278  3cubes  39294  ismrc  39305  isnacs3  39314  rexzrexnn0  39408  eldioph4b  39415  dford3  39632  wopprc  39634  ttac  39640  pw2f1ocnv  39641  dfac11  39669  dfac21  39673  isnumbasabl  39713  isnumbasgrp  39714  dfacbasgrp  39715  aaitgo  39769  ifpbi1b  39876  rp-fakeimass  39885  rp-fakeanorass  39886  rp-isfinite5  39890  rp-isfinite6  39891  dfsucon  39896  snen1g  39897  iscard4  39907  rtrclex  39984  cnvtrrel  40022  rp-imass  40124  frege54cor0a  40216  isotone1  40405  isotone2  40406  gneispace  40491  k0004lem3  40506  grumnueq  40630  nanorxor  40644  nzss  40656  pm10.55  40708  pm11.57  40728  pm13.192  40749  pm13.194  40751  ipo0  40788  ifr0  40789  xpexb  40793  3impexpbicom  40820  com3rgbi  40855  pm2.43bgbi  40858  pm2.43cbi  40859  sb5ALT  40866  trsbc  40881  2pm13.193  40893  ax6e2ndeq  40900  2uasbanh  40902  eelT01  41052  eel0T1  41053  uunT1  41121  zfregs2VD  41182  equncomVD  41209  trsbcVD  41218  undif3VD  41223  2pm13.193VD  41244  ax6e2eqVD  41248  ax6e2ndeqVD  41250  2uasbanhVD  41252  ax6e2ndeqALT  41272  fompt  41460  mptssid  41518  elfzfzo  41549  allbutfi  41672  uzn0bi  41742  dvnprodlem3  42240  elaa2  42526  sge00  42665  elhoi  42831  ovn0  42855  ovolval4lem2  42939  confun  43182  afvfv0bi  43358  ffnafv  43377  afv2ndefb  43430  dfatafv2rnb  43433  afv2fv0b  43472  dfich2OLD  43623  prpair  43670  sbcpr  43690  fpprel2  43913  sbgoldbmb  43958  mgm2mgm  44141  isringrng  44159  nnpw2pb  44654  elsetrecs  44809  elpg  44823