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  3488  gencbvex2  3489  pm13.183  3609  rr19.3v  3610  rr19.28v  3611  euxfr2w  3667  euxfr2  3669  reu6  3673  reu3  3674  reuan  3835  dfss2  3908  sspss  4043  complss  4092  unineq  4229  uneqin  4230  difrab  4259  sbnfc2  4380  un00  4386  ssdifeq0  4427  r19.2zb  4441  ralidmw  4457  ralidm  4458  pwidb  4563  snidb  4606  rabsnifsb  4667  tppreqb  4749  difsnb  4750  pwpw0  4757  sssn  4770  preq12b  4794  unissint  4915  uniintsn  4928  iununi  5042  al0ssb  5243  intex  5281  intnex  5282  axpweq  5288  iin0  5299  nfcvb  5313  eusvnfb  5330  eusv2nf  5332  ralxfrALT  5352  sspwb  5396  unipw  5397  opnz  5421  opth  5424  sbcop1  5436  opeqsng  5451  propeqop  5455  opthwiener  5462  opthhausdorff  5465  opthhausdorff0  5466  rexopabb  5476  ssopab2bw  5495  ssopab2b  5497  pwssun  5516  opelxp  5660  opthprc  5688  relsnb  5751  relop  5799  issetid  5803  xpid11  5881  elinxp  5978  eldmeldmressn  5984  iss  5994  iresn0n0  6013  asymref2  6074  xpnz  6117  xpdifid  6126  ssrnres  6136  dfrel2  6147  resssxp  6228  relrelss  6231  unixp0  6241  reuop  6251  dfpo2  6254  fn0  6623  funssxp  6690  f00  6716  f0bi  6717  dffo2  6750  f1o00  6809  fo00  6810  fv3  6852  dffn5  6892  dff2  7045  dff3  7046  dffo4  7049  dffo5  7050  exfo  7051  fmpt  7056  fompt  7064  ffnfv  7065  fsn  7082  fsn2  7083  funop  7096  funsneqopb  7099  fnsnbOLD  7114  isores1  7282  ssoprab2b  7429  eqoprab2bw  7430  eqfnov2  7490  unexb  7694  unexbOLD  7695  uniexb  7711  pwexb  7713  iunpw  7718  ordeleqon  7729  dford5  7731  onintrab  7743  ordsuc  7758  unon  7775  onuninsuci  7784  ordzsl  7789  onzsl  7790  f1oexbi  7872  ffoss  7892  1st2ndb  7975  frxp3  8094  suppssov1  8140  suppssov2  8141  suppssfv  8145  reldmtpos  8177  dfrecs3  8305  omopthi  8590  brinxper  8666  ecopover  8761  fsetexb  8804  mapsncnv  8834  mptelixpg  8876  elixpsn  8878  ixpsnf1o  8879  bren2  8923  en0  8958  en0ALT  8959  en0r  8960  en1  8964  en1b  8965  sbthb  9029  dom0  9036  canth2  9061  onfin2  9144  sdom1  9153  1sdom2dom  9157  fineqv  9170  unfilem1  9208  unfib  9212  pwfir  9220  pwfi  9222  fiint  9230  residfi  9241  unifpw  9258  wofib  9453  sucprcreg  9512  opthreg  9530  suc11reg  9531  infeq5  9549  rankwflemb  9708  r1elss  9721  pwwf  9722  unwf  9725  uniwf  9734  rankonid  9744  rankr1id  9777  rankuni  9778  rankxplim3  9796  scott0  9801  karden  9810  djuexb  9824  isnum3  9869  oncard  9875  card1  9883  cardlim  9887  cardmin2  9914  pm54.43lem  9915  ween  9948  acnnum  9965  alephsuc2  9993  alephgeom  9995  iscard3  10006  dfac3  10034  dfac4  10035  dfac5lem3  10038  dfac5  10042  dfac2  10045  dfac8  10049  dfac9  10050  dfacacn  10055  dfac13  10056  dfac12r  10060  dfac12k  10061  kmlem2  10065  kmlem13  10076  djuinf  10102  ackbij2  10155  cflim2  10176  isfin4-2  10227  isfin4p1  10228  isf33lem  10279  compsscnv  10284  fin1a2lem6  10318  domtriom  10356  ac9  10396  ac9s  10406  fodomb  10439  brdom3  10441  brdom5  10442  brdom4  10443  brdom7disj  10444  brdom6disj  10445  iunfo  10452  sdomsdomcard  10473  gch2  10589  gch3  10590  eltsk2g  10665  grutsk  10736  ordpipq  10856  ltbtwnnq  10892  mappsrpr  11022  map2psrpr  11024  elreal2  11046  le2tri3i  11267  elnn0nn  12470  elnnnn0b  12472  elnnnn0c  12473  elnnz  12525  elnn0z  12528  elz2  12533  elnnz1  12544  eluz2b2  12862  elnn1uz2  12866  elpqb  12917  elioo4g  13350  eluzfz2b  13478  fzn0  13483  elfz1end  13499  fzass4  13507  elfz1b  13538  nn0fz0  13570  fzolb  13611  fzon0  13623  elfzo0  13646  elfzo0z  13647  elfzo1  13658  fzo1fzo0n0  13661  om2uzrani  13905  nn0opthi  14223  hashkf  14285  isfinite4  14315  hashprb  14350  hashf1  14410  elss2prb  14441  iswrdb  14473  wrdexb  14478  0wrd0  14493  wrdl3s3  14915  cotr2g  14929  trclun  14967  rexanuz  15299  rexuz3  15302  fsum0diag  15730  fprod0diag  15942  divalgmod  16366  sadcp1  16415  isprm6  16675  nnoddn2prmb  16775  4sqlem4  16914  fnpr2ob  17513  mreunirn  17554  isdrs2  18263  isacs5  18505  isacs4  18506  isacs3  18507  dfgrp2  18929  dfgrp3  19006  dfgrp3e  19007  isnsg3  19126  gicer  19243  oppgmndb  19321  oppggrpb  19324  pmtrfb  19431  invghm  19799  isringrng  20259  opprrngb  20317  opprringb  20319  isnzr2hash  20487  isdomn4  20684  abvn0b  20804  gzrngunit  21423  dvdsrzring  21451  zringunit  21456  zlmlmod  21512  cygth  21561  frgpcyg  21563  zlmassa  21893  toprntopon  22900  tgclb  22945  iscldtop  23070  isnrm2  23333  isnrm3  23334  discmp  23373  dfconn2  23394  2ndcsb  23424  dis2ndc  23435  loclly  23462  unisngl  23502  locfindis  23505  iskgen2  23523  dfac14  23593  kqtop  23720  kqt0  23721  kqreg  23726  kqnrm  23727  hmpher  23759  hmphsymb  23761  hmph0  23770  kqhmph  23794  ist1-5lem  23795  elmptrab2  23803  isfil2  23831  filunirn  23857  isufil2  23883  hausflim  23956  isfcls  23984  alexsubALT  24026  istgp2  24066  ustbas  24202  xmetunirn  24312  dscmet  24547  dscopn  24548  isngp4  24587  zcld  24789  zlmclm  25089  iscmet2  25271  iundisj  25525  i1f1lem  25666  fta1b  26147  elply2  26171  elqaa  26299  aannenlem2  26306  wilth  27048  lgsne0  27312  2lgs  27384  2sqlem2  27395  ostth  27616  elno2  27632  bdayfo  27655  elons2  28264  eln0s2  28363  eln0s  28367  elzn0s  28404  eln0zs  28406  elnnzs  28407  remulscllem1  28506  mpteleeOLD  28978  wrdupgr  29168  wrdumgr  29180  umgrislfupgr  29206  uspgrupgrushgr  29262  usgrumgruspgr  29265  usgruspgrb  29266  usgrislfuspgr  29270  uvtx01vtx  29480  pthspthcyc  29886  wwlksnwwlksnon  29998  elwwlks2ons3  30038  clwwlkn1loopb  30128  eclclwwlkn1  30160  upgriseupth  30292  numclwwlkovh  30458  nmlno0lem  30879  isblo3i  30887  blocni  30891  hvsubeq0i  31149  hvaddcani  31151  bcseqi  31206  isch3  31327  norm1exi  31336  hhsssh  31355  shslubi  31471  dfch2  31493  pjoc1i  31517  pjchi  31518  shs00i  31536  chsscon3i  31547  chlejb1i  31562  chj00i  31573  shjshseli  31579  h1de2ctlem  31641  spanunsni  31665  cmcmi  31678  cmbr3i  31686  cmbr4i  31687  pj11i  31797  hosubeq0i  31912  dmadjrnb  31992  nmlnop0iALT  32081  lnopeq0i  32093  elunop2  32099  lnconi  32119  lncnopbd  32123  adjbdlnb  32170  adjbd1o  32171  adjeq0  32177  rnbra  32193  pjss1coi  32249  pjss2coi  32250  pjnormssi  32254  pjssdif2i  32260  pjssdif1i  32261  dfpjop  32268  pjinvari  32277  pjin2i  32279  pjci  32286  pjcmul1i  32287  pjcmul2i  32288  strb  32344  hstrbi  32352  mdsl1i  32407  atom1d  32439  chrelat2i  32451  cvbr4i  32453  cvexchi  32455  sumdmdi  32506  dmdbr4ati  32507  dmdbr5ati  32508  dmdbr6ati  32509  dmdbr7ati  32510  cdj3i  32527  eqtrb  32558  difeq  32603  iundisjf  32674  fpwrelmap  32821  iundisjfi  32884  xrge0tsmsbi  33150  dfufd2  33625  ccfldextdgrr  33832  issgon  34283  measbasedom  34362  oddpwdc  34514  eulerpartlemt  34531  ballotlem2  34649  ballotlemrinv  34694  bnj1533  35010  bnj983  35109  r1omhf  35265  r1omhfb  35272  fineqvomonb  35279  fineqvnttrclse  35284  r1omhfbregs  35297  fineqvr1ombregs  35298  0nn0m1nnn0  35311  lfuhgr3  35318  spthcycl  35327  satfv1  35561  satf0op  35575  fmla0xp  35581  fmla1  35585  elmsta  35746  antnestlaw1  35889  antnestlaw2  35890  antnestlaw3  35891  nepss  35916  dfon2  35988  distel  35999  fnimage  36125  altopthsn  36159  ellines  36350  rankeq1o  36369  opnrebl2  36519  df3nandALT1  36597  ttc00  36706  ttcwf  36722  ttcwf2  36723  ttcexbi  36731  ttc0el  36733  bj-animbi  36839  bj-dfbi6  36856  bj-consensus  36859  bj-falor2  36866  bj-bibibi  36867  bj-andnotim  36869  bj-alextruim  36947  bj-exextruan  36948  bj-ssbeq  36963  bj-19.41al  36969  bj-subst  36971  bj-eqs  36986  bj-cbvexw  36987  bj-sb  37000  bj-substax12  37037  bj-dfnnf3  37094  bj-equs45fv  37134  bj-hbaeb2  37141  bj-hbnaeb  37143  bj-equsal  37149  bj-sbsb  37160  bj-moeub  37172  bj-csbsnlem  37226  bj-snsetex  37286  bj-snglex  37296  bj-1uplth  37330  bj-1uplex  37331  bj-2uplth  37344  bj-2uplex  37345  bj-bm1.3ii  37387  bj-restpw  37420  bj-restuni  37425  bj-discrmoore  37439  bj-snmooreb  37442  bj-elid6  37500  bj-eldiag2  37507  mptsnunlem  37668  topdifinf  37679  elxp8  37701  finxp1o  37722  wl-moae  37855  wl-exeq  37873  wl-aleq  37874  wl-nfeqfb  37875  volsupnfl  38000  cover2  38050  isbnd3  38119  cntotbnd  38131  heibor  38156  isfld2  38340  isfldidl  38403  orfa  38417  eqbrb  38574  eqelb  38576  iss2  38679  issetssr  38918  n0el3  39071  detlem  39221  petlem  39250  eldisjs6  39275  prtlem16  39329  isltrn2N  40580  aks6d1c2p2  42572  aks6d1c6isolem3  42629  sn-iotalem  42676  dffltz  43081  eu6w  43123  3cubes  43136  ismrc  43147  isnacs3  43156  rexzrexnn0  43250  eldioph4b  43257  dford3  43474  wopprc  43476  ttac  43482  pw2f1ocnv  43483  dfac11  43508  dfac21  43512  isnumbasabl  43552  isnumbasgrp  43553  dfacbasgrp  43554  aaitgo  43608  dflim5  43775  nvocnvb  43867  dfno2  43873  ifpbi1b  43948  rp-fakeimass  43957  rp-fakeanorass  43958  rp-isfinite5  43962  rp-isfinite6  43963  dfsucon  43968  snen1g  43969  iscard4  43978  rtrclex  44062  cnvtrrel  44115  frege54cor0a  44308  isotone1  44493  isotone2  44494  gneispace  44579  k0004lem3  44594  grumnueq  44732  ismnushort  44746  nanorxor  44750  nzss  44762  pm10.55  44814  pm11.57  44834  pm13.192  44855  pm13.194  44857  ipo0  44893  ifr0  44894  xpexb  44898  3impexpbicom  44925  com3rgbi  44959  pm2.43bgbi  44962  pm2.43cbi  44963  sb5ALT  44970  trsbc  44985  2pm13.193  44997  ax6e2ndeq  45004  2uasbanh  45006  eelT01  45155  eel0T1  45156  uunT1  45224  zfregs2VD  45285  equncomVD  45312  trsbcVD  45321  undif3VD  45326  2pm13.193VD  45347  ax6e2eqVD  45351  ax6e2ndeqVD  45353  2uasbanhVD  45355  ax6e2ndeqALT  45375  tcfr  45408  mptssid  45688  elfzfzo  45728  allbutfi  45840  uzn0bi  45905  dvnprodlem3  46394  elaa2  46680  sge00  46822  elhoi  46988  ovn0  47012  ovolval4lem2  47096  confun  47399  afvfv0bi  47612  ffnafv  47631  afv2ndefb  47684  dfatafv2rnb  47687  afv2fv0b  47726  prpair  47973  sbcpr  47993  fpprel2  48229  sbgoldbmb  48274  vopnbgrelself  48343  isgrtri  48431  stgr1  48449  mgm2mgm  48715  nnpw2pb  49075  0aryfvalel  49122  mo0sn  49303  resinsnlem  49358  homf0  49496  isoval2  49522  oppccicb  49538  oppcciceq  49539  funcf2lem2  49569  initc  49578  isinito2  49986  isinito3  49987  termc  50006  dftermc3  50018  elsetrecs  50187  elpg  50201