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  315  con34b  316  notbi  319  bibi2i  338  con1b  359  con2b  360  bi2.04  389  imdi  391  pm4.8  393  pm4.81  394  impexp  451  ancom  461  anass  469  jcab  518  impimprbi  826  orcom  867  dfor2  899  oridm  902  orbi2i  910  or12  918  biorfi  936  pm4.72  947  oibabs  949  jaob  959  pm4.44  994  pm4.79  1001  andi  1005  pm4.82  1021  cases2ALT  1046  consensus  1050  3impexp  1357  3jaob  1425  nanass  1505  norassOLD  1536  tbw-bijust  1701  tbw-negdf  1702  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  2157  19.3  2196  19.41  2229  sbalex  2236  equsexv  2261  sbim  2301  cbvalv1  2339  cbval  2399  equsex  2419  aecom  2428  equs45f  2460  dfsb1  2486  dfsb2  2498  sb6f  2502  dfmoeu  2537  moabs  2544  mobii  2549  mo3  2565  mo4  2567  exmoeu  2582  moanimlem  2621  euan  2624  euanv  2627  2mo  2651  2eu6  2659  euae  2662  axextb  2713  eqcom  2746  nebi  3025  r19.26  3096  r19.21v  3114  r19.35  3272  ralcom3  3292  cgsex4g  3477  ceqsex  3479  ceqsexv  3480  gencbvex  3489  gencbvex2  3490  pm13.183  3598  rr19.3v  3599  rr19.28v  3600  euxfr2w  3656  euxfr2  3658  reu6  3662  reu3  3663  reuan  3830  sspss  4035  complss  4082  unineq  4212  uneqin  4213  difrab  4243  ab0w  4308  sbnfc2  4371  un00  4377  disj  4382  ssdifeq0  4418  r19.2zb  4427  ralidmw  4439  ralidm  4443  ralf0  4445  pwidb  4557  snidb  4597  rabsnifsb  4659  tppreqb  4739  difsnb  4740  pwpw0  4747  sssn  4760  preq12b  4782  pwsnOLD  4833  unissint  4904  uniintsn  4919  iununi  5029  al0ssb  5233  intex  5262  intnex  5263  iin0  5285  axpweq  5288  nfcvb  5300  eusvnfb  5317  eusv2nf  5319  ralxfrALT  5339  sspwb  5366  unipw  5367  opnz  5389  opth  5392  sbcop1  5403  opeqsng  5418  propeqop  5422  opthwiener  5429  opthhausdorff  5432  opthhausdorff0  5433  rexopabb  5442  ssopab2bw  5461  ssopab2b  5463  pwssun  5486  opelxp  5626  opthprc  5652  relsnb  5714  relop  5762  issetid  5766  xpid11  5844  elinxp  5932  eldmeldmressn  5938  iss  5946  iresn0n0  5966  asymref2  6027  xpnz  6067  xpdifid  6076  ssrnres  6086  dfrel2  6097  resssxp  6177  relrelss  6180  unixp0  6190  reuop  6200  dfpo2  6203  fn0  6573  funssxp  6638  f00  6665  f0bi  6666  dffo2  6701  f1o00  6760  fo00  6761  fv3  6801  dffn5  6837  dff2  6984  dff3  6985  dffo4  6988  dffo5  6989  exfo  6990  fmpt  6993  ffnfv  7001  fsn  7016  fsn2  7017  funop  7030  funsneqopb  7033  fnsnb  7047  isores1  7214  ssoprab2b  7353  eqoprab2bw  7354  eqfnov2  7413  unexb  7607  uniexb  7623  pwexb  7625  iunpw  7630  ordeleqon  7641  onintrab  7655  unon  7687  onuninsuci  7696  ordzsl  7701  onzsl  7702  f1oexbi  7784  ffoss  7797  1st2ndb  7880  suppssov1  8023  suppssfv  8027  reldmtpos  8059  dfrecs3  8212  dfrecs3OLD  8213  omopthi  8500  ecopover  8619  fsetexb  8661  mapsncnv  8690  mptelixpg  8732  elixpsn  8734  ixpsnf1o  8735  bren2  8780  en0  8812  en0OLD  8813  en0ALT  8814  en0r  8815  en1  8820  en1OLD  8821  en1b  8822  en1bOLD  8823  sbthb  8890  dom0  8898  canth2  8926  pwfir  8968  pwfi  8970  onfin2  9023  sdom1  9031  1sdom  9034  fineqv  9047  unfilem1  9087  fiint  9100  residfi  9109  pwfiOLD  9123  unifpw  9131  wofib  9313  sucprcreg  9369  opthreg  9385  suc11reg  9386  infeq5  9404  rankwflemb  9560  r1elss  9573  pwwf  9574  unwf  9577  uniwf  9586  rankonid  9596  rankr1id  9629  rankuni  9630  rankxplim3  9648  scott0  9653  karden  9662  djuexb  9676  isnum3  9721  oncard  9727  card1  9735  cardlim  9739  cardmin2  9766  pm54.43lem  9767  ween  9800  acnnum  9817  alephsuc2  9845  alephgeom  9847  iscard3  9858  dfac3  9886  dfac4  9887  dfac5lem3  9890  dfac5  9893  dfac2  9896  dfac8  9900  dfac9  9901  dfacacn  9906  dfac13  9907  dfac12r  9911  dfac12k  9912  kmlem2  9916  kmlem13  9927  djuinf  9953  ackbij2  10008  cflim2  10028  isfin4-2  10079  isfin4p1  10080  isf33lem  10131  compsscnv  10136  fin1a2lem6  10170  domtriom  10208  ac9  10248  ac9s  10258  fodomb  10291  brdom3  10293  brdom5  10294  brdom4  10295  brdom7disj  10296  brdom6disj  10297  iunfo  10304  sdomsdomcard  10325  gch2  10440  gch3  10441  eltsk2g  10516  grutsk  10587  ordpipq  10707  ltbtwnnq  10743  mappsrpr  10873  map2psrpr  10875  elreal2  10897  le2tri3i  11114  elnn0nn  12284  elnnnn0b  12286  elnnnn0c  12287  elnnz  12338  elnn0z  12341  elz2  12346  elnnz1  12355  eluz2b2  12670  elnn1uz2  12674  elpqb  12725  elioo4g  13148  eluzfz2b  13274  fzn0  13279  elfz1end  13295  fzass4  13303  elfz1b  13334  nn0fz0  13363  fzolb  13402  fzon0  13414  elfzo0  13437  elfzo0z  13438  elfzo1  13446  fzo1fzo0n0  13447  om2uzrani  13681  nn0opthi  13993  hashkf  14055  isfinite4  14086  hashprb  14121  hashf1  14180  elss2prb  14210  iswrdb  14232  wrdexb  14237  0wrd0  14252  wrdl3s3  14686  cotr2g  14696  trclun  14734  sqr0lem  14961  rexanuz  15066  rexuz3  15069  fsum0diag  15498  fprod0diag  15705  divalgmod  16124  sadcp1  16171  isprm6  16428  nnoddn2prmb  16523  4sqlem4  16662  fnpr2ob  17278  mreunirn  17319  isdrs2  18033  isacs5  18275  isacs4  18276  isacs3  18277  dfgrp2  18613  dfgrp3  18683  dfgrp3e  18684  isnsg3  18797  gicer  18901  oppgmndb  18971  oppggrpb  18974  pmtrfb  19082  invghm  19444  opprringb  19883  isnzr2hash  20544  abvn0b  20582  gzrngunit  20673  dvdsrzring  20692  zringunit  20697  zlmlmod  20737  cygth  20788  frgpcyg  20790  zlmassa  21115  toprntopon  22083  tgclb  22129  iscldtop  22255  isnrm2  22518  isnrm3  22519  discmp  22558  dfconn2  22579  2ndcsb  22609  dis2ndc  22620  loclly  22647  unisngl  22687  locfindis  22690  iskgen2  22708  dfac14  22778  kqtop  22905  kqt0  22906  kqreg  22911  kqnrm  22912  hmpher  22944  hmphsymb  22946  hmph0  22955  kqhmph  22979  ist1-5lem  22980  elmptrab2  22988  isfil2  23016  filunirn  23042  isufil2  23068  hausflim  23141  isfcls  23169  alexsubALT  23211  istgp2  23251  ustbas  23388  xmetunirn  23499  dscmet  23737  dscopn  23738  isngp4  23777  zcld  23985  zlmclm  24284  iscmet2  24467  iundisj  24721  i1f1lem  24862  fta1b  25343  elply2  25366  elqaa  25491  aannenlem2  25498  wilth  26229  lgsne0  26492  2lgs  26564  2sqlem2  26575  ostth  26796  mptelee  27272  wrdupgr  27464  wrdumgr  27476  umgrislfupgr  27502  uspgrupgrushgr  27556  usgrumgruspgr  27559  usgruspgrb  27560  usgrislfuspgr  27563  uvtx01vtx  27773  wwlksnwwlksnon  28289  elwwlks2ons3  28329  clwwlkn1loopb  28416  eclclwwlkn1  28448  upgriseupth  28580  numclwwlkovh  28746  nmlno0lem  29164  isblo3i  29172  blocni  29176  hvsubeq0i  29434  hvaddcani  29436  bcseqi  29491  isch3  29612  norm1exi  29621  hhsssh  29640  shslubi  29756  dfch2  29778  pjoc1i  29802  pjchi  29803  shs00i  29821  chsscon3i  29832  chlejb1i  29847  chj00i  29858  shjshseli  29864  h1de2ctlem  29926  spanunsni  29950  cmcmi  29963  cmbr3i  29971  cmbr4i  29972  pj11i  30082  hosubeq0i  30197  dmadjrnb  30277  nmlnop0iALT  30366  lnopeq0i  30378  elunop2  30384  lnconi  30404  lncnopbd  30408  adjbdlnb  30455  adjbd1o  30456  adjeq0  30462  rnbra  30478  pjss1coi  30534  pjss2coi  30535  pjnormssi  30539  pjssdif2i  30545  pjssdif1i  30546  dfpjop  30553  pjinvari  30562  pjin2i  30564  pjci  30571  pjcmul1i  30572  pjcmul2i  30573  strb  30629  hstrbi  30637  mdsl1i  30692  atom1d  30724  chrelat2i  30736  cvbr4i  30738  cvexchi  30740  sumdmdi  30791  dmdbr4ati  30792  dmdbr5ati  30793  dmdbr6ati  30794  dmdbr7ati  30795  cdj3i  30812  eqtrb  30832  difeq  30874  iundisjf  30937  cnvoprabOLD  31064  fpwrelmap  31077  iundisjfi  31126  xrge0tsmsbi  31327  ccfldextdgrr  31751  issgon  32100  measbasedom  32179  oddpwdc  32330  eulerpartlemt  32347  ballotlem2  32464  ballotlemrinv  32509  bnj1533  32841  bnj983  32940  0nn0m1nnn0  33080  lfuhgr3  33090  spthcycl  33100  satfv1  33334  satf0op  33348  fmla0xp  33354  fmla1  33358  elmsta  33519  nepss  33671  dford5  33680  dfon2  33777  distel  33788  frxp3  33806  elno2  33866  bdayfo  33889  fnimage  34240  altopthsn  34272  ellines  34463  rankeq1o  34482  opnrebl2  34519  df3nandALT1  34597  bj-animbi  34748  bj-dfbi6  34765  bj-consensus  34768  bj-falor2  34776  bj-bibibi  34777  bj-andnotim  34779  bj-cbval  34839  bj-cbvex  34840  bj-ssbeq  34843  bj-19.41al  34849  bj-subst  34851  bj-eqs  34865  bj-cbvexw  34866  bj-sb  34878  bj-substax12  34912  bj-dfnnf3  34948  bj-equs45fv  35002  bj-hbaeb2  35010  bj-hbnaeb  35012  bj-equsal  35018  bj-sbsb  35029  bj-moeub  35042  bj-csbsnlem  35097  bj-snsetex  35162  bj-snglex  35172  bj-1uplth  35206  bj-1uplex  35207  bj-2uplth  35220  bj-2uplex  35221  bj-bm1.3ii  35244  bj-restpw  35272  bj-restuni  35277  bj-discrmoore  35291  bj-snmooreb  35294  bj-elid6  35350  bj-eldiag2  35357  mptsnunlem  35518  topdifinf  35529  elxp8  35551  finxp1o  35572  wl-moae  35684  wl-exeq  35702  wl-aleq  35703  wl-nfeqfb  35704  wl-ax11-lem6  35750  volsupnfl  35831  cover2  35881  isbnd3  35951  cntotbnd  35963  heibor  35988  isfld2  36172  isfldidl  36235  orfa  36249  eqelb  36391  iss2  36486  issetssr  36628  n0el3  36770  prtlem16  36890  isltrn2N  38141  isdomn4  40179  sn-iotalem  40196  dffltz  40478  3cubes  40519  ismrc  40530  isnacs3  40539  rexzrexnn0  40633  eldioph4b  40640  dford3  40857  wopprc  40859  ttac  40865  pw2f1ocnv  40866  dfac11  40894  dfac21  40898  isnumbasabl  40938  isnumbasgrp  40939  dfacbasgrp  40940  aaitgo  40994  ifpbi1b  41117  rp-fakeimass  41126  rp-fakeanorass  41127  rp-isfinite5  41131  rp-isfinite6  41132  dfsucon  41137  snen1g  41138  iscard4  41147  rtrclex  41232  cnvtrrel  41285  frege54cor0a  41478  isotone1  41665  isotone2  41666  gneispace  41751  k0004lem3  41766  grumnueq  41912  ismnushort  41926  nanorxor  41930  nzss  41942  pm10.55  41994  pm11.57  42014  pm13.192  42035  pm13.194  42037  ipo0  42074  ifr0  42075  xpexb  42079  3impexpbicom  42106  com3rgbi  42141  pm2.43bgbi  42144  pm2.43cbi  42145  sb5ALT  42152  trsbc  42167  2pm13.193  42179  ax6e2ndeq  42186  2uasbanh  42188  eelT01  42338  eel0T1  42339  uunT1  42407  zfregs2VD  42468  equncomVD  42495  trsbcVD  42504  undif3VD  42509  2pm13.193VD  42530  ax6e2eqVD  42534  ax6e2ndeqVD  42536  2uasbanhVD  42538  ax6e2ndeqALT  42558  fompt  42737  mptssid  42792  elfzfzo  42822  allbutfi  42940  uzn0bi  43006  dvnprodlem3  43496  elaa2  43782  sge00  43921  elhoi  44087  ovn0  44111  ovolval4lem2  44195  confun  44445  afvfv0bi  44655  ffnafv  44674  afv2ndefb  44727  dfatafv2rnb  44730  afv2fv0b  44769  prpair  44964  sbcpr  44984  fpprel2  45204  sbgoldbmb  45249  mgm2mgm  45432  isringrng  45450  nnpw2pb  45944  0aryfvalel  45991  mo0sn  46172  elsetrecs  46416  elpg  46430