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  829  orcom  871  dfor2  902  oridm  905  orbi2i  913  or12  921  biorfriOLD  941  pm4.72  952  oibabs  954  jaob  964  pm4.44  999  pm4.79  1006  andi  1010  pm4.82  1026  cases2ALT  1049  consensus  1053  3impexp  1360  3jaobOLD  1430  nanass  1512  tbw-bijust  1700  tbw-negdf  1701  19.26  1872  19.35  1879  19.21v  1941  19.23v  1944  19.41v  1951  19.3v  1984  19.9v  1986  equcom  2020  cbvalw  2037  alcomw  2047  excomw  2048  exexw  2055  sbbii  2082  sban  2086  sbv  2094  alcom  2165  19.3  2210  19.41  2243  sbalex  2250  sbalexOLD  2251  equsexv  2276  sbim  2310  cbvalv1  2346  cbval  2403  equsex  2423  aecom  2432  equs45f  2464  dfsb1  2486  dfsb2  2498  sb6f  2502  dfmoeu  2536  moabs  2544  mo3  2565  mo4  2567  exmoeu  2582  moanimlem  2619  euan  2622  euanv  2625  2mo  2649  2eu6  2658  euae  2661  axextb  2712  eqcom  2744  nebi  3013  r19.35  3096  r19.26  3098  r19.21v  3163  gencbvex  3501  gencbvex2  3502  pm13.183  3622  rr19.3v  3623  rr19.28v  3624  euxfr2w  3680  euxfr2  3682  reu6  3686  reu3  3687  reuan  3848  dfss2  3921  sspss  4056  complss  4105  unineq  4242  uneqin  4243  difrab  4272  sbnfc2  4393  un00  4399  ssdifeq0  4441  r19.2zb  4455  ralidmw  4471  ralidm  4472  pwidb  4577  snidb  4620  rabsnifsb  4681  tppreqb  4763  difsnb  4764  pwpw0  4771  sssn  4784  preq12b  4808  unissint  4929  uniintsn  4942  iununi  5056  al0ssb  5255  intex  5291  intnex  5292  axpweq  5298  iin0  5309  nfcvb  5323  eusvnfb  5340  eusv2nf  5342  ralxfrALT  5362  sspwb  5404  unipw  5405  opnz  5429  opth  5432  sbcop1  5444  opeqsng  5459  propeqop  5463  opthwiener  5470  opthhausdorff  5473  opthhausdorff0  5474  rexopabb  5484  ssopab2bw  5503  ssopab2b  5505  pwssun  5524  opelxp  5668  opthprc  5696  relsnb  5759  relop  5807  issetid  5811  xpid11  5889  elinxp  5986  eldmeldmressn  5992  iss  6002  iresn0n0  6021  asymref2  6082  xpnz  6125  xpdifid  6134  ssrnres  6144  dfrel2  6155  resssxp  6236  relrelss  6239  unixp0  6249  reuop  6259  dfpo2  6262  fn0  6631  funssxp  6698  f00  6724  f0bi  6725  dffo2  6758  f1o00  6817  fo00  6818  fv3  6860  dffn5  6900  dff2  7053  dff3  7054  dffo4  7057  dffo5  7058  exfo  7059  fmpt  7064  fompt  7072  ffnfv  7073  fsn  7090  fsn2  7091  funop  7104  funsneqopb  7107  fnsnbOLD  7122  isores1  7290  ssoprab2b  7437  eqoprab2bw  7438  eqfnov2  7498  unexb  7702  unexbOLD  7703  uniexb  7719  pwexb  7721  iunpw  7726  ordeleqon  7737  dford5  7739  onintrab  7751  ordsuc  7766  unon  7783  onuninsuci  7792  ordzsl  7797  onzsl  7798  f1oexbi  7880  ffoss  7900  1st2ndb  7983  frxp3  8103  suppssov1  8149  suppssov2  8150  suppssfv  8154  reldmtpos  8186  dfrecs3  8314  omopthi  8599  brinxper  8675  ecopover  8770  fsetexb  8813  mapsncnv  8843  mptelixpg  8885  elixpsn  8887  ixpsnf1o  8888  bren2  8932  en0  8967  en0ALT  8968  en0r  8969  en1  8973  en1b  8974  sbthb  9038  dom0  9045  canth2  9070  onfin2  9153  sdom1  9162  1sdom2dom  9166  fineqv  9179  unfilem1  9217  unfib  9221  pwfir  9229  pwfi  9231  fiint  9239  residfi  9250  unifpw  9267  wofib  9462  sucprcreg  9521  opthreg  9539  suc11reg  9540  infeq5  9558  rankwflemb  9717  r1elss  9730  pwwf  9731  unwf  9734  uniwf  9743  rankonid  9753  rankr1id  9786  rankuni  9787  rankxplim3  9805  scott0  9810  karden  9819  djuexb  9833  isnum3  9878  oncard  9884  card1  9892  cardlim  9896  cardmin2  9923  pm54.43lem  9924  ween  9957  acnnum  9974  alephsuc2  10002  alephgeom  10004  iscard3  10015  dfac3  10043  dfac4  10044  dfac5lem3  10047  dfac5  10051  dfac2  10054  dfac8  10058  dfac9  10059  dfacacn  10064  dfac13  10065  dfac12r  10069  dfac12k  10070  kmlem2  10074  kmlem13  10085  djuinf  10111  ackbij2  10164  cflim2  10185  isfin4-2  10236  isfin4p1  10237  isf33lem  10288  compsscnv  10293  fin1a2lem6  10327  domtriom  10365  ac9  10405  ac9s  10415  fodomb  10448  brdom3  10450  brdom5  10451  brdom4  10452  brdom7disj  10453  brdom6disj  10454  iunfo  10461  sdomsdomcard  10482  gch2  10598  gch3  10599  eltsk2g  10674  grutsk  10745  ordpipq  10865  ltbtwnnq  10901  mappsrpr  11031  map2psrpr  11033  elreal2  11055  le2tri3i  11275  elnn0nn  12455  elnnnn0b  12457  elnnnn0c  12458  elnnz  12510  elnn0z  12513  elz2  12518  elnnz1  12529  eluz2b2  12846  elnn1uz2  12850  elpqb  12901  elioo4g  13334  eluzfz2b  13461  fzn0  13466  elfz1end  13482  fzass4  13490  elfz1b  13521  nn0fz0  13553  fzolb  13593  fzon0  13605  elfzo0  13628  elfzo0z  13629  elfzo1  13640  fzo1fzo0n0  13643  om2uzrani  13887  nn0opthi  14205  hashkf  14267  isfinite4  14297  hashprb  14332  hashf1  14392  elss2prb  14423  iswrdb  14455  wrdexb  14460  0wrd0  14475  wrdl3s3  14897  cotr2g  14911  trclun  14949  rexanuz  15281  rexuz3  15284  fsum0diag  15712  fprod0diag  15921  divalgmod  16345  sadcp1  16394  isprm6  16653  nnoddn2prmb  16753  4sqlem4  16892  fnpr2ob  17491  mreunirn  17532  isdrs2  18241  isacs5  18483  isacs4  18484  isacs3  18485  dfgrp2  18904  dfgrp3  18981  dfgrp3e  18982  isnsg3  19101  gicer  19218  oppgmndb  19296  oppggrpb  19299  pmtrfb  19406  invghm  19774  isringrng  20234  opprrngb  20294  opprringb  20296  isnzr2hash  20464  isdomn4  20661  abvn0b  20781  gzrngunit  21400  dvdsrzring  21428  zringunit  21433  zlmlmod  21489  cygth  21538  frgpcyg  21540  zlmassa  21871  toprntopon  22881  tgclb  22926  iscldtop  23051  isnrm2  23314  isnrm3  23315  discmp  23354  dfconn2  23375  2ndcsb  23405  dis2ndc  23416  loclly  23443  unisngl  23483  locfindis  23486  iskgen2  23504  dfac14  23574  kqtop  23701  kqt0  23702  kqreg  23707  kqnrm  23708  hmpher  23740  hmphsymb  23742  hmph0  23751  kqhmph  23775  ist1-5lem  23776  elmptrab2  23784  isfil2  23812  filunirn  23838  isufil2  23864  hausflim  23937  isfcls  23965  alexsubALT  24007  istgp2  24047  ustbas  24183  xmetunirn  24293  dscmet  24528  dscopn  24529  isngp4  24568  zcld  24770  zlmclm  25080  iscmet2  25262  iundisj  25517  i1f1lem  25658  fta1b  26145  elply2  26169  elqaa  26298  aannenlem2  26305  wilth  27049  lgsne0  27314  2lgs  27386  2sqlem2  27397  ostth  27618  elno2  27634  bdayfo  27657  elons2  28266  eln0s2  28365  eln0s  28369  elzn0s  28406  eln0zs  28408  elnnzs  28409  remulscllem1  28508  mpteleeOLD  28980  wrdupgr  29170  wrdumgr  29182  umgrislfupgr  29208  uspgrupgrushgr  29264  usgrumgruspgr  29267  usgruspgrb  29268  usgrislfuspgr  29272  uvtx01vtx  29482  pthspthcyc  29888  wwlksnwwlksnon  30000  elwwlks2ons3  30040  clwwlkn1loopb  30130  eclclwwlkn1  30162  upgriseupth  30294  numclwwlkovh  30460  nmlno0lem  30881  isblo3i  30889  blocni  30893  hvsubeq0i  31151  hvaddcani  31153  bcseqi  31208  isch3  31329  norm1exi  31338  hhsssh  31357  shslubi  31473  dfch2  31495  pjoc1i  31519  pjchi  31520  shs00i  31538  chsscon3i  31549  chlejb1i  31564  chj00i  31575  shjshseli  31581  h1de2ctlem  31643  spanunsni  31667  cmcmi  31680  cmbr3i  31688  cmbr4i  31689  pj11i  31799  hosubeq0i  31914  dmadjrnb  31994  nmlnop0iALT  32083  lnopeq0i  32095  elunop2  32101  lnconi  32121  lncnopbd  32125  adjbdlnb  32172  adjbd1o  32173  adjeq0  32179  rnbra  32195  pjss1coi  32251  pjss2coi  32252  pjnormssi  32256  pjssdif2i  32262  pjssdif1i  32263  dfpjop  32270  pjinvari  32279  pjin2i  32281  pjci  32288  pjcmul1i  32289  pjcmul2i  32290  strb  32346  hstrbi  32354  mdsl1i  32409  atom1d  32441  chrelat2i  32453  cvbr4i  32455  cvexchi  32457  sumdmdi  32508  dmdbr4ati  32509  dmdbr5ati  32510  dmdbr6ati  32511  dmdbr7ati  32512  cdj3i  32529  eqtrb  32560  difeq  32605  iundisjf  32676  fpwrelmap  32823  iundisjfi  32887  xrge0tsmsbi  33168  dfufd2  33643  ccfldextdgrr  33850  issgon  34301  measbasedom  34380  oddpwdc  34532  eulerpartlemt  34549  ballotlem2  34667  ballotlemrinv  34712  bnj1533  35028  bnj983  35127  r1omhf  35283  r1omhfb  35290  fineqvomonb  35297  fineqvnttrclse  35302  r1omhfbregs  35315  fineqvr1ombregs  35316  0nn0m1nnn0  35329  lfuhgr3  35336  spthcycl  35345  satfv1  35579  satf0op  35593  fmla0xp  35599  fmla1  35603  elmsta  35764  antnestlaw1  35907  antnestlaw2  35908  antnestlaw3  35909  nepss  35934  dfon2  36006  distel  36017  fnimage  36143  altopthsn  36177  ellines  36368  rankeq1o  36387  opnrebl2  36537  df3nandALT1  36615  bj-animbi  36783  bj-dfbi6  36800  bj-consensus  36803  bj-falor2  36810  bj-bibibi  36811  bj-andnotim  36813  bj-alextruim  36880  bj-exextruan  36881  bj-cbval  36893  bj-cbvex  36894  bj-ssbeq  36898  bj-19.41al  36904  bj-subst  36906  bj-eqs  36920  bj-cbvexw  36921  bj-sb  36932  bj-substax12  36967  bj-dfnnf3  37019  bj-equs45fv  37059  bj-hbaeb2  37066  bj-hbnaeb  37068  bj-equsal  37074  bj-sbsb  37085  bj-moeub  37097  bj-csbsnlem  37151  bj-snsetex  37211  bj-snglex  37221  bj-1uplth  37255  bj-1uplex  37256  bj-2uplth  37269  bj-2uplex  37270  bj-bm1.3ii  37312  bj-restpw  37345  bj-restuni  37350  bj-discrmoore  37364  bj-snmooreb  37367  bj-elid6  37425  bj-eldiag2  37432  mptsnunlem  37593  topdifinf  37604  elxp8  37626  finxp1o  37647  wl-moae  37771  wl-exeq  37789  wl-aleq  37790  wl-nfeqfb  37791  volsupnfl  37916  cover2  37966  isbnd3  38035  cntotbnd  38047  heibor  38072  isfld2  38256  isfldidl  38319  orfa  38333  eqbrb  38490  eqelb  38492  iss2  38595  issetssr  38834  n0el3  38987  detlem  39137  petlem  39166  eldisjs6  39191  prtlem16  39245  isltrn2N  40496  aks6d1c2p2  42489  aks6d1c6isolem3  42546  sn-iotalem  42593  dffltz  42992  eu6w  43034  3cubes  43047  ismrc  43058  isnacs3  43067  rexzrexnn0  43161  eldioph4b  43168  dford3  43385  wopprc  43387  ttac  43393  pw2f1ocnv  43394  dfac11  43419  dfac21  43423  isnumbasabl  43463  isnumbasgrp  43464  dfacbasgrp  43465  aaitgo  43519  dflim5  43686  nvocnvb  43778  dfno2  43784  ifpbi1b  43859  rp-fakeimass  43868  rp-fakeanorass  43869  rp-isfinite5  43873  rp-isfinite6  43874  dfsucon  43879  snen1g  43880  iscard4  43889  rtrclex  43973  cnvtrrel  44026  frege54cor0a  44219  isotone1  44404  isotone2  44405  gneispace  44490  k0004lem3  44505  grumnueq  44643  ismnushort  44657  nanorxor  44661  nzss  44673  pm10.55  44725  pm11.57  44745  pm13.192  44766  pm13.194  44768  ipo0  44804  ifr0  44805  xpexb  44809  3impexpbicom  44836  com3rgbi  44870  pm2.43bgbi  44873  pm2.43cbi  44874  sb5ALT  44881  trsbc  44896  2pm13.193  44908  ax6e2ndeq  44915  2uasbanh  44917  eelT01  45066  eel0T1  45067  uunT1  45135  zfregs2VD  45196  equncomVD  45223  trsbcVD  45232  undif3VD  45237  2pm13.193VD  45258  ax6e2eqVD  45262  ax6e2ndeqVD  45264  2uasbanhVD  45266  ax6e2ndeqALT  45286  tcfr  45319  mptssid  45599  elfzfzo  45639  allbutfi  45751  uzn0bi  45817  dvnprodlem3  46306  elaa2  46592  sge00  46734  elhoi  46900  ovn0  46924  ovolval4lem2  47008  confun  47299  afvfv0bi  47512  ffnafv  47531  afv2ndefb  47584  dfatafv2rnb  47587  afv2fv0b  47626  prpair  47861  sbcpr  47881  fpprel2  48101  sbgoldbmb  48146  vopnbgrelself  48215  isgrtri  48303  stgr1  48321  mgm2mgm  48587  nnpw2pb  48947  0aryfvalel  48994  mo0sn  49175  resinsnlem  49230  homf0  49368  isoval2  49394  oppccicb  49410  oppcciceq  49411  funcf2lem2  49441  initc  49450  isinito2  49858  isinito3  49859  termc  49878  dftermc3  49890  elsetrecs  50059  elpg  50073