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  337  con1b  358  con2b  359  bi2.04  388  imdi  390  pm4.8  392  pm4.81  393  impexp  450  ancom  460  anass  468  jcab  517  impimprbi  825  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  1045  consensus  1049  3impexp  1356  3jaob  1424  nanass  1502  norassOLD  1536  tbw-bijust  1702  tbw-negdf  1703  19.26  1874  19.35  1881  19.21v  1943  19.23v  1946  19.41v  1954  19.3v  1986  19.9v  1988  equcom  2022  cbvalw  2039  exexw  2055  sbbii  2080  sban  2084  sbv  2092  alcom  2158  19.3  2198  19.41  2231  sbalex  2238  equsexv  2263  sbim  2303  cbvalv1  2340  cbval  2398  equsex  2418  aecom  2427  equs45f  2459  dfsb1  2485  dfsb2  2497  sb6f  2501  dfmoeu  2536  moabs  2543  mobii  2548  mo3  2564  mo4  2566  exmoeu  2581  moanimlem  2620  euan  2623  euanv  2626  2mo  2650  2eu6  2658  euae  2661  axextb  2712  eqcom  2745  nebi  3023  r19.26  3094  r19.35  3268  ralcom3  3289  cgsex4g  3466  ceqsex  3468  ceqsexv  3469  gencbvex  3478  gencbvex2  3479  pm13.183  3590  rr19.3v  3591  rr19.28v  3592  euxfr2w  3650  euxfr2  3652  reu6  3656  reu3  3657  reuan  3825  sspss  4030  complss  4077  unineq  4208  uneqin  4209  difrab  4239  ab0w  4304  sbnfc2  4367  un00  4373  disj  4378  ssdifeq0  4414  r19.2zb  4423  ralidmw  4435  ralidm  4439  ralf0  4441  pwidb  4553  snidb  4593  rabsnifsb  4655  tppreqb  4735  difsnb  4736  pwpw0  4743  sssn  4756  preq12b  4778  pwsnOLD  4829  unissint  4900  uniintsn  4915  iununi  5024  al0ssb  5227  intex  5256  intnex  5257  iin0  5279  axpweq  5282  nfcvb  5294  eusvnfb  5311  eusv2nf  5313  ralxfrALT  5333  sspwb  5359  unipw  5360  opnz  5382  opth  5385  sbcop1  5396  opeqsng  5411  propeqop  5415  opthwiener  5422  opthhausdorff  5425  opthhausdorff0  5426  rexopabb  5434  ssopab2bw  5453  ssopab2b  5455  pwssun  5476  opelxp  5616  opthprc  5642  relsnb  5701  relop  5748  issetid  5752  xpid11  5830  elinxp  5918  eldmeldmressn  5924  iss  5932  iresn0n0  5952  asymref2  6011  xpnz  6051  xpdifid  6060  ssrnres  6070  dfrel2  6081  resssxp  6162  relrelss  6165  unixp0  6175  reuop  6185  dfpo2  6188  fn0  6548  funssxp  6613  f00  6640  f0bi  6641  dffo2  6676  f1o00  6734  fo00  6735  fv3  6774  dffn5  6810  dff2  6957  dff3  6958  dffo4  6961  dffo5  6962  exfo  6963  fmpt  6966  ffnfv  6974  fsn  6989  fsn2  6990  funop  7003  funsneqopb  7006  fnsnb  7020  isores1  7185  ssoprab2b  7322  eqoprab2bw  7323  eqfnov2  7382  unexb  7576  uniexb  7592  pwexb  7594  iunpw  7599  ordeleqon  7609  onintrab  7623  unon  7653  onuninsuci  7662  ordzsl  7667  onzsl  7668  f1oexbi  7749  ffoss  7762  1st2ndb  7844  suppssov1  7985  suppssfv  7989  reldmtpos  8021  dfrecs3  8174  dfrecs3OLD  8175  omopthi  8451  ecopover  8568  fsetexb  8610  mapsncnv  8639  mptelixpg  8681  elixpsn  8683  ixpsnf1o  8684  bren2  8726  en0  8758  en0OLD  8759  en0ALT  8760  en1  8765  en1OLD  8766  en1b  8767  en1bOLD  8768  sbthb  8834  canth2  8866  pwfir  8921  pwfi  8923  onfin2  8945  sdom1  8952  1sdom  8955  fineqv  8967  unfilem1  9008  fiint  9021  residfi  9030  pwfiOLD  9044  unifpw  9052  wofib  9234  sucprcreg  9290  opthreg  9306  suc11reg  9307  infeq5  9325  rankwflemb  9482  r1elss  9495  pwwf  9496  unwf  9499  uniwf  9508  rankonid  9518  rankr1id  9551  rankuni  9552  rankxplim3  9570  scott0  9575  karden  9584  djuexb  9598  isnum3  9643  oncard  9649  card1  9657  cardlim  9661  cardmin2  9688  pm54.43lem  9689  ween  9722  acnnum  9739  alephsuc2  9767  alephgeom  9769  iscard3  9780  dfac3  9808  dfac4  9809  dfac5lem3  9812  dfac5  9815  dfac2  9818  dfac8  9822  dfac9  9823  dfacacn  9828  dfac13  9829  dfac12r  9833  dfac12k  9834  kmlem2  9838  kmlem13  9849  djuinf  9875  ackbij2  9930  cflim2  9950  isfin4-2  10001  isfin4p1  10002  isf33lem  10053  compsscnv  10058  fin1a2lem6  10092  domtriom  10130  ac9  10170  ac9s  10180  fodomb  10213  brdom3  10215  brdom5  10216  brdom4  10217  brdom7disj  10218  brdom6disj  10219  iunfo  10226  sdomsdomcard  10247  gch2  10362  gch3  10363  eltsk2g  10438  grutsk  10509  ordpipq  10629  ltbtwnnq  10665  mappsrpr  10795  map2psrpr  10797  elreal2  10819  le2tri3i  11035  elnn0nn  12205  elnnnn0b  12207  elnnnn0c  12208  elnnz  12259  elnn0z  12262  elz2  12267  elnnz1  12276  eluz2b2  12590  elnn1uz2  12594  elpqb  12645  elioo4g  13068  eluzfz2b  13194  fzn0  13199  elfz1end  13215  fzass4  13223  elfz1b  13254  nn0fz0  13283  fzolb  13322  fzon0  13333  elfzo0  13356  elfzo0z  13357  elfzo1  13365  fzo1fzo0n0  13366  om2uzrani  13600  nn0opthi  13912  hashkf  13974  isfinite4  14005  hashprb  14040  hashf1  14099  elss2prb  14129  iswrdb  14151  wrdexb  14156  0wrd0  14171  wrdl3s3  14605  cotr2g  14615  trclun  14653  sqr0lem  14880  rexanuz  14985  rexuz3  14988  fsum0diag  15417  fprod0diag  15624  divalgmod  16043  sadcp1  16090  isprm6  16347  nnoddn2prmb  16442  4sqlem4  16581  fnpr2ob  17186  mreunirn  17227  isdrs2  17939  isacs5  18181  isacs4  18182  isacs3  18183  dfgrp2  18519  dfgrp3  18589  dfgrp3e  18590  isnsg3  18703  gicer  18807  oppgmndb  18877  oppggrpb  18880  pmtrfb  18988  invghm  19350  opprringb  19789  isnzr2hash  20448  abvn0b  20486  gzrngunit  20576  dvdsrzring  20595  zringunit  20600  zlmlmod  20640  cygth  20691  frgpcyg  20693  zlmassa  21016  toprntopon  21982  tgclb  22028  iscldtop  22154  isnrm2  22417  isnrm3  22418  discmp  22457  dfconn2  22478  2ndcsb  22508  dis2ndc  22519  loclly  22546  unisngl  22586  locfindis  22589  iskgen2  22607  dfac14  22677  kqtop  22804  kqt0  22805  kqreg  22810  kqnrm  22811  hmpher  22843  hmphsymb  22845  hmph0  22854  kqhmph  22878  ist1-5lem  22879  elmptrab2  22887  isfil2  22915  filunirn  22941  isufil2  22967  hausflim  23040  isfcls  23068  alexsubALT  23110  istgp2  23150  ustbas  23287  xmetunirn  23398  dscmet  23634  dscopn  23635  isngp4  23674  zcld  23882  zlmclm  24181  iscmet2  24363  iundisj  24617  i1f1lem  24758  fta1b  25239  elply2  25262  elqaa  25387  aannenlem2  25394  wilth  26125  lgsne0  26388  2lgs  26460  2sqlem2  26471  ostth  26692  mptelee  27166  wrdupgr  27358  wrdumgr  27370  umgrislfupgr  27396  uspgrupgrushgr  27450  usgrumgruspgr  27453  usgruspgrb  27454  usgrislfuspgr  27457  uvtx01vtx  27667  wwlksnwwlksnon  28181  elwwlks2ons3  28221  clwwlkn1loopb  28308  eclclwwlkn1  28340  upgriseupth  28472  numclwwlkovh  28638  nmlno0lem  29056  isblo3i  29064  blocni  29068  hvsubeq0i  29326  hvaddcani  29328  bcseqi  29383  isch3  29504  norm1exi  29513  hhsssh  29532  shslubi  29648  dfch2  29670  pjoc1i  29694  pjchi  29695  shs00i  29713  chsscon3i  29724  chlejb1i  29739  chj00i  29750  shjshseli  29756  h1de2ctlem  29818  spanunsni  29842  cmcmi  29855  cmbr3i  29863  cmbr4i  29864  pj11i  29974  hosubeq0i  30089  dmadjrnb  30169  nmlnop0iALT  30258  lnopeq0i  30270  elunop2  30276  lnconi  30296  lncnopbd  30300  adjbdlnb  30347  adjbd1o  30348  adjeq0  30354  rnbra  30370  pjss1coi  30426  pjss2coi  30427  pjnormssi  30431  pjssdif2i  30437  pjssdif1i  30438  dfpjop  30445  pjinvari  30454  pjin2i  30456  pjci  30463  pjcmul1i  30464  pjcmul2i  30465  strb  30521  hstrbi  30529  mdsl1i  30584  atom1d  30616  chrelat2i  30628  cvbr4i  30630  cvexchi  30632  sumdmdi  30683  dmdbr4ati  30684  dmdbr5ati  30685  dmdbr6ati  30686  dmdbr7ati  30687  cdj3i  30704  eqtrb  30724  difeq  30766  iundisjf  30829  cnvoprabOLD  30957  fpwrelmap  30970  iundisjfi  31019  xrge0tsmsbi  31220  ccfldextdgrr  31644  issgon  31991  measbasedom  32070  oddpwdc  32221  eulerpartlemt  32238  ballotlem2  32355  ballotlemrinv  32400  bnj1533  32732  bnj983  32831  0nn0m1nnn0  32971  lfuhgr3  32981  spthcycl  32991  satfv1  33225  satf0op  33239  fmla0xp  33245  fmla1  33249  elmsta  33410  nepss  33564  dford5  33573  dfon2  33674  distel  33685  frxp3  33724  elno2  33784  bdayfo  33807  fnimage  34158  altopthsn  34190  ellines  34381  rankeq1o  34400  opnrebl2  34437  df3nandALT1  34515  bj-animbi  34666  bj-dfbi6  34683  bj-consensus  34686  bj-falor2  34694  bj-bibibi  34695  bj-andnotim  34697  bj-cbval  34757  bj-cbvex  34758  bj-ssbeq  34761  bj-19.41al  34767  bj-subst  34769  bj-eqs  34783  bj-cbvexw  34784  bj-sb  34796  bj-substax12  34830  bj-dfnnf3  34866  bj-equs45fv  34920  bj-hbaeb2  34928  bj-hbnaeb  34930  bj-equsal  34936  bj-sbsb  34947  bj-moeub  34960  bj-csbsnlem  35015  bj-snsetex  35080  bj-snglex  35090  bj-1uplth  35124  bj-1uplex  35125  bj-2uplth  35138  bj-2uplex  35139  bj-bm1.3ii  35162  bj-restpw  35190  bj-restuni  35195  bj-discrmoore  35209  bj-snmooreb  35212  bj-elid6  35268  bj-eldiag2  35275  mptsnunlem  35436  topdifinf  35447  elxp8  35469  finxp1o  35490  wl-moae  35602  wl-exeq  35620  wl-aleq  35621  wl-nfeqfb  35622  wl-ax11-lem6  35668  volsupnfl  35749  cover2  35799  isbnd3  35869  cntotbnd  35881  heibor  35906  isfld2  36090  isfldidl  36153  orfa  36167  eqelb  36309  iss2  36406  issetssr  36548  n0el3  36690  prtlem16  36810  isltrn2N  38061  isdomn4  40100  sn-iotalem  40117  dffltz  40387  3cubes  40428  ismrc  40439  isnacs3  40448  rexzrexnn0  40542  eldioph4b  40549  dford3  40766  wopprc  40768  ttac  40774  pw2f1ocnv  40775  dfac11  40803  dfac21  40807  isnumbasabl  40847  isnumbasgrp  40848  dfacbasgrp  40849  aaitgo  40903  ifpbi1b  41008  rp-fakeimass  41017  rp-fakeanorass  41018  rp-isfinite5  41022  rp-isfinite6  41023  dfsucon  41028  snen1g  41029  iscard4  41038  rtrclex  41114  cnvtrrel  41167  frege54cor0a  41360  isotone1  41547  isotone2  41548  gneispace  41633  k0004lem3  41648  grumnueq  41794  ismnushort  41808  nanorxor  41812  nzss  41824  pm10.55  41876  pm11.57  41896  pm13.192  41917  pm13.194  41919  ipo0  41956  ifr0  41957  xpexb  41961  3impexpbicom  41988  com3rgbi  42023  pm2.43bgbi  42026  pm2.43cbi  42027  sb5ALT  42034  trsbc  42049  2pm13.193  42061  ax6e2ndeq  42068  2uasbanh  42070  eelT01  42220  eel0T1  42221  uunT1  42289  zfregs2VD  42350  equncomVD  42377  trsbcVD  42386  undif3VD  42391  2pm13.193VD  42412  ax6e2eqVD  42416  ax6e2ndeqVD  42418  2uasbanhVD  42420  ax6e2ndeqALT  42440  fompt  42619  mptssid  42674  elfzfzo  42704  allbutfi  42823  uzn0bi  42889  dvnprodlem3  43379  elaa2  43665  sge00  43804  elhoi  43970  ovn0  43994  ovolval4lem2  44078  confun  44321  afvfv0bi  44531  ffnafv  44550  afv2ndefb  44603  dfatafv2rnb  44606  afv2fv0b  44645  prpair  44841  sbcpr  44861  fpprel2  45081  sbgoldbmb  45126  mgm2mgm  45309  isringrng  45327  nnpw2pb  45821  0aryfvalel  45868  mo0sn  46049  elsetrecs  46291  elpg  46305