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  393  pm4.81  394  impexp  451  ancom  461  anass  469  jcab  518  impimprbi  827  orcom  868  dfor2  900  oridm  903  orbi2i  911  or12  919  biorfi  937  pm4.72  948  oibabs  950  jaob  960  pm4.44  995  pm4.79  1002  andi  1006  pm4.82  1022  cases2ALT  1047  consensus  1051  3impexp  1358  3jaob  1426  nanass  1508  tbw-bijust  1700  tbw-negdf  1701  19.26  1873  19.35  1880  19.21v  1942  19.23v  1945  19.41v  1953  19.3v  1985  19.9v  1987  equcom  2021  cbvalw  2038  alcomw  2047  exexw  2054  sbbii  2079  sban  2083  sbv  2091  alcom  2156  19.3  2195  19.41  2228  sbalex  2235  equsexv  2259  sbim  2299  cbvalv1  2337  cbval  2397  equsex  2417  aecom  2426  equs45f  2458  dfsb1  2480  dfsb2  2492  sb6f  2496  dfmoeu  2530  moabs  2537  mobii  2542  mo3  2558  mo4  2560  exmoeu  2575  moanimlem  2614  euan  2617  euanv  2620  2mo  2644  2eu6  2652  euae  2655  axextb  2706  eqcom  2739  nebi  3021  ralcom3OLD  3098  r19.35  3108  r19.35OLD  3109  r19.26  3111  r19.21v  3179  ceqsexOLD  3524  ceqsexvOLD  3526  gencbvex  3535  gencbvex2  3536  pm13.183  3656  rr19.3v  3657  rr19.28v  3658  euxfr2w  3716  euxfr2  3718  reu6  3722  reu3  3723  reuan  3890  sspss  4099  complss  4146  unineq  4277  uneqin  4278  difrab  4308  ab0w  4373  sbnfc2  4436  un00  4442  disj  4447  ssdifeq0  4486  r19.2zb  4495  ralidmw  4507  ralidm  4511  ralf0  4513  pwidb  4623  snidb  4663  rabsnifsb  4726  tppreqb  4808  difsnb  4809  pwpw0  4816  sssn  4829  preq12b  4851  pwsnOLD  4901  unissint  4976  uniintsn  4991  iununi  5102  al0ssb  5308  intex  5337  intnex  5338  axpweq  5348  iin0  5360  nfcvb  5374  eusvnfb  5391  eusv2nf  5393  ralxfrALT  5413  sspwb  5449  unipw  5450  opnz  5473  opth  5476  sbcop1  5488  opeqsng  5503  propeqop  5507  opthwiener  5514  opthhausdorff  5517  opthhausdorff0  5518  rexopabb  5528  ssopab2bw  5547  ssopab2b  5549  pwssun  5571  opelxp  5712  opthprc  5740  relsnb  5802  relop  5850  issetid  5854  xpid11  5931  elinxp  6019  eldmeldmressn  6025  iss  6035  iresn0n0  6053  asymref2  6118  xpnz  6158  xpdifid  6167  ssrnres  6177  dfrel2  6188  resssxp  6269  relrelss  6272  unixp0  6282  reuop  6292  dfpo2  6295  fn0  6681  funssxp  6746  f00  6773  f0bi  6774  dffo2  6809  f1o00  6868  fo00  6869  fv3  6909  dffn5  6950  dff2  7100  dff3  7101  dffo4  7104  dffo5  7105  exfo  7106  fmpt  7111  fompt  7119  ffnfv  7120  fsn  7135  fsn2  7136  funop  7149  funsneqopb  7152  fnsnb  7166  isores1  7333  ssoprab2b  7480  eqoprab2bw  7481  eqfnov2  7541  unexb  7737  uniexb  7753  pwexb  7755  iunpw  7760  ordeleqon  7771  dford5  7773  onintrab  7786  ordsuc  7803  unon  7821  onuninsuci  7831  ordzsl  7836  onzsl  7837  f1oexbi  7921  ffoss  7934  1st2ndb  8017  frxp3  8139  suppssov1  8185  suppssfv  8189  reldmtpos  8221  dfrecs3  8374  dfrecs3OLD  8375  omopthi  8662  ecopover  8817  fsetexb  8860  mapsncnv  8889  mptelixpg  8931  elixpsn  8933  ixpsnf1o  8934  bren2  8981  en0  9015  en0OLD  9016  en0ALT  9017  en0r  9018  en1  9023  en1OLD  9024  en1b  9025  en1bOLD  9026  sbthb  9096  dom0  9104  canth2  9132  pwfir  9178  pwfi  9180  onfin2  9233  sdom1  9244  sdom1OLD  9245  1sdom2dom  9249  1sdomOLD  9251  fineqv  9265  unfilem1  9312  fiint  9326  residfi  9335  pwfiOLD  9349  unifpw  9357  wofib  9542  sucprcreg  9598  opthreg  9615  suc11reg  9616  infeq5  9634  rankwflemb  9790  r1elss  9803  pwwf  9804  unwf  9807  uniwf  9816  rankonid  9826  rankr1id  9859  rankuni  9860  rankxplim3  9878  scott0  9883  karden  9892  djuexb  9906  isnum3  9951  oncard  9957  card1  9965  cardlim  9969  cardmin2  9996  pm54.43lem  9997  ween  10032  acnnum  10049  alephsuc2  10077  alephgeom  10079  iscard3  10090  dfac3  10118  dfac4  10119  dfac5lem3  10122  dfac5  10125  dfac2  10128  dfac8  10132  dfac9  10133  dfacacn  10138  dfac13  10139  dfac12r  10143  dfac12k  10144  kmlem2  10148  kmlem13  10159  djuinf  10185  ackbij2  10240  cflim2  10260  isfin4-2  10311  isfin4p1  10312  isf33lem  10363  compsscnv  10368  fin1a2lem6  10402  domtriom  10440  ac9  10480  ac9s  10490  fodomb  10523  brdom3  10525  brdom5  10526  brdom4  10527  brdom7disj  10528  brdom6disj  10529  iunfo  10536  sdomsdomcard  10557  gch2  10672  gch3  10673  eltsk2g  10748  grutsk  10819  ordpipq  10939  ltbtwnnq  10975  mappsrpr  11105  map2psrpr  11107  elreal2  11129  le2tri3i  11348  elnn0nn  12518  elnnnn0b  12520  elnnnn0c  12521  elnnz  12572  elnn0z  12575  elz2  12580  elnnz1  12592  eluz2b2  12909  elnn1uz2  12913  elpqb  12964  elioo4g  13388  eluzfz2b  13514  fzn0  13519  elfz1end  13535  fzass4  13543  elfz1b  13574  nn0fz0  13603  fzolb  13642  fzon0  13654  elfzo0  13677  elfzo0z  13678  elfzo1  13686  fzo1fzo0n0  13687  om2uzrani  13921  nn0opthi  14234  hashkf  14296  isfinite4  14326  hashprb  14361  hashf1  14422  elss2prb  14452  iswrdb  14474  wrdexb  14479  0wrd0  14494  wrdl3s3  14917  cotr2g  14927  trclun  14965  rexanuz  15296  rexuz3  15299  fsum0diag  15727  fprod0diag  15934  divalgmod  16353  sadcp1  16400  isprm6  16655  nnoddn2prmb  16750  4sqlem4  16889  fnpr2ob  17508  mreunirn  17549  isdrs2  18263  isacs5  18505  isacs4  18506  isacs3  18507  dfgrp2  18883  dfgrp3  18958  dfgrp3e  18959  isnsg3  19076  gicer  19191  oppgmndb  19263  oppggrpb  19266  pmtrfb  19374  invghm  19742  isringrng  20175  opprrngb  20237  opprringb  20239  isnzr2hash  20410  isdomn4  21118  abvn0b  21120  gzrngunit  21211  dvdsrzring  21232  zringunit  21237  zlmlmod  21295  cygth  21346  frgpcyg  21348  zlmassa  21675  toprntopon  22647  tgclb  22693  iscldtop  22819  isnrm2  23082  isnrm3  23083  discmp  23122  dfconn2  23143  2ndcsb  23173  dis2ndc  23184  loclly  23211  unisngl  23251  locfindis  23254  iskgen2  23272  dfac14  23342  kqtop  23469  kqt0  23470  kqreg  23475  kqnrm  23476  hmpher  23508  hmphsymb  23510  hmph0  23519  kqhmph  23543  ist1-5lem  23544  elmptrab2  23552  isfil2  23580  filunirn  23606  isufil2  23632  hausflim  23705  isfcls  23733  alexsubALT  23775  istgp2  23815  ustbas  23952  xmetunirn  24063  dscmet  24301  dscopn  24302  isngp4  24341  zcld  24549  zlmclm  24852  iscmet2  25035  iundisj  25289  i1f1lem  25430  fta1b  25911  elply2  25934  elqaa  26059  aannenlem2  26066  wilth  26799  lgsne0  27062  2lgs  27134  2sqlem2  27145  ostth  27366  elno2  27381  bdayfo  27404  elons2  27912  mptelee  28408  wrdupgr  28600  wrdumgr  28612  umgrislfupgr  28638  uspgrupgrushgr  28692  usgrumgruspgr  28695  usgruspgrb  28696  usgrislfuspgr  28699  uvtx01vtx  28909  wwlksnwwlksnon  29424  elwwlks2ons3  29464  clwwlkn1loopb  29551  eclclwwlkn1  29583  upgriseupth  29715  numclwwlkovh  29881  nmlno0lem  30301  isblo3i  30309  blocni  30313  hvsubeq0i  30571  hvaddcani  30573  bcseqi  30628  isch3  30749  norm1exi  30758  hhsssh  30777  shslubi  30893  dfch2  30915  pjoc1i  30939  pjchi  30940  shs00i  30958  chsscon3i  30969  chlejb1i  30984  chj00i  30995  shjshseli  31001  h1de2ctlem  31063  spanunsni  31087  cmcmi  31100  cmbr3i  31108  cmbr4i  31109  pj11i  31219  hosubeq0i  31334  dmadjrnb  31414  nmlnop0iALT  31503  lnopeq0i  31515  elunop2  31521  lnconi  31541  lncnopbd  31545  adjbdlnb  31592  adjbd1o  31593  adjeq0  31599  rnbra  31615  pjss1coi  31671  pjss2coi  31672  pjnormssi  31676  pjssdif2i  31682  pjssdif1i  31683  dfpjop  31690  pjinvari  31699  pjin2i  31701  pjci  31708  pjcmul1i  31709  pjcmul2i  31710  strb  31766  hstrbi  31774  mdsl1i  31829  atom1d  31861  chrelat2i  31873  cvbr4i  31875  cvexchi  31877  sumdmdi  31928  dmdbr4ati  31929  dmdbr5ati  31930  dmdbr6ati  31931  dmdbr7ati  31932  cdj3i  31949  eqtrb  31969  difeq  32011  iundisjf  32075  cnvoprabOLD  32200  fpwrelmap  32213  iundisjfi  32262  xrge0tsmsbi  32468  ccfldextdgrr  33023  issgon  33407  measbasedom  33486  oddpwdc  33639  eulerpartlemt  33656  ballotlem2  33773  ballotlemrinv  33818  bnj1533  34149  bnj983  34248  0nn0m1nnn0  34388  lfuhgr3  34396  spthcycl  34406  satfv1  34640  satf0op  34654  fmla0xp  34660  fmla1  34664  elmsta  34825  nepss  34979  dfon2  35056  distel  35067  fnimage  35193  altopthsn  35225  ellines  35416  rankeq1o  35435  opnrebl2  35509  df3nandALT1  35587  bj-animbi  35738  bj-dfbi6  35755  bj-consensus  35758  bj-falor2  35766  bj-bibibi  35767  bj-andnotim  35769  bj-cbval  35829  bj-cbvex  35830  bj-ssbeq  35833  bj-19.41al  35839  bj-subst  35841  bj-eqs  35855  bj-cbvexw  35856  bj-sb  35868  bj-substax12  35902  bj-dfnnf3  35938  bj-equs45fv  35992  bj-hbaeb2  35999  bj-hbnaeb  36001  bj-equsal  36007  bj-sbsb  36018  bj-moeub  36031  bj-csbsnlem  36086  bj-snsetex  36147  bj-snglex  36157  bj-1uplth  36191  bj-1uplex  36192  bj-2uplth  36205  bj-2uplex  36206  bj-bm1.3ii  36248  bj-restpw  36276  bj-restuni  36281  bj-discrmoore  36295  bj-snmooreb  36298  bj-elid6  36354  bj-eldiag2  36361  mptsnunlem  36522  topdifinf  36533  elxp8  36555  finxp1o  36576  wl-moae  36688  wl-exeq  36706  wl-aleq  36707  wl-nfeqfb  36708  wl-ax11-lem6  36755  volsupnfl  36836  cover2  36886  isbnd3  36955  cntotbnd  36967  heibor  36992  isfld2  37176  isfldidl  37239  orfa  37253  eqbrb  37402  eqelb  37404  iss2  37516  issetssr  37676  n0el3  37824  detlem  37956  petlem  37985  prtlem16  38042  isltrn2N  39294  aks6d1c2p2  41263  sn-iotalem  41344  dffltz  41678  3cubes  41730  ismrc  41741  isnacs3  41750  rexzrexnn0  41844  eldioph4b  41851  dford3  42069  wopprc  42071  ttac  42077  pw2f1ocnv  42078  dfac11  42106  dfac21  42110  isnumbasabl  42150  isnumbasgrp  42151  dfacbasgrp  42152  aaitgo  42206  dflim5  42381  nvocnvb  42475  dfno2  42481  ifpbi1b  42556  rp-fakeimass  42565  rp-fakeanorass  42566  rp-isfinite5  42570  rp-isfinite6  42571  dfsucon  42576  snen1g  42577  iscard4  42586  rtrclex  42670  cnvtrrel  42723  frege54cor0a  42916  isotone1  43101  isotone2  43102  gneispace  43187  k0004lem3  43202  grumnueq  43348  ismnushort  43362  nanorxor  43366  nzss  43378  pm10.55  43430  pm11.57  43450  pm13.192  43471  pm13.194  43473  ipo0  43510  ifr0  43511  xpexb  43515  3impexpbicom  43542  com3rgbi  43577  pm2.43bgbi  43580  pm2.43cbi  43581  sb5ALT  43588  trsbc  43603  2pm13.193  43615  ax6e2ndeq  43622  2uasbanh  43624  eelT01  43774  eel0T1  43775  uunT1  43843  zfregs2VD  43904  equncomVD  43931  trsbcVD  43940  undif3VD  43945  2pm13.193VD  43966  ax6e2eqVD  43970  ax6e2ndeqVD  43972  2uasbanhVD  43974  ax6e2ndeqALT  43994  mptssid  44243  elfzfzo  44285  allbutfi  44402  uzn0bi  44468  dvnprodlem3  44963  elaa2  45249  sge00  45391  elhoi  45557  ovn0  45581  ovolval4lem2  45665  confun  45948  afvfv0bi  46159  ffnafv  46178  afv2ndefb  46231  dfatafv2rnb  46234  afv2fv0b  46273  prpair  46468  sbcpr  46488  fpprel2  46708  sbgoldbmb  46753  mgm2mgm  46904  nnpw2pb  47361  0aryfvalel  47408  mo0sn  47588  elsetrecs  47833  elpg  47847