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  828  orcom  870  dfor2  901  oridm  904  orbi2i  912  or12  920  biorfriOLD  940  pm4.72  951  oibabs  953  jaob  963  pm4.44  998  pm4.79  1005  andi  1009  pm4.82  1025  cases2ALT  1048  consensus  1052  3impexp  1359  3jaobOLD  1429  nanass  1511  tbw-bijust  1699  tbw-negdf  1700  19.26  1871  19.35  1878  19.21v  1940  19.23v  1943  19.41v  1950  19.3v  1983  19.9v  1985  equcom  2019  cbvalw  2036  alcomw  2046  excomw  2047  exexw  2054  sbbii  2081  sban  2085  sbv  2093  alcom  2164  19.3  2207  19.41  2240  sbalex  2247  sbalexOLD  2248  equsexv  2273  sbim  2307  cbvalv1  2343  cbval  2400  equsex  2420  aecom  2429  equs45f  2461  dfsb1  2483  dfsb2  2495  sb6f  2499  dfmoeu  2533  moabs  2540  mobii  2545  mo3  2561  mo4  2563  exmoeu  2578  moanimlem  2615  euan  2618  euanv  2621  2mo  2645  2eu6  2654  euae  2657  axextb  2708  eqcom  2740  nebi  3009  r19.35  3091  r19.26  3093  r19.21v  3158  gencbvex  3496  gencbvex2  3497  pm13.183  3617  rr19.3v  3618  rr19.28v  3619  euxfr2w  3675  euxfr2  3677  reu6  3681  reu3  3682  reuan  3843  dfss2  3916  sspss  4051  complss  4100  unineq  4237  uneqin  4238  difrab  4267  sbnfc2  4388  un00  4394  ssdifeq0  4436  r19.2zb  4450  ralidmw  4466  ralidm  4467  pwidb  4572  snidb  4615  rabsnifsb  4676  tppreqb  4758  difsnb  4759  pwpw0  4766  sssn  4779  preq12b  4803  unissint  4924  uniintsn  4937  iununi  5051  al0ssb  5250  intex  5286  intnex  5287  axpweq  5293  iin0  5304  nfcvb  5318  eusvnfb  5335  eusv2nf  5337  ralxfrALT  5357  sspwb  5394  unipw  5395  opnz  5418  opth  5421  sbcop1  5433  opeqsng  5448  propeqop  5452  opthwiener  5459  opthhausdorff  5462  opthhausdorff0  5463  rexopabb  5473  ssopab2bw  5492  ssopab2b  5494  pwssun  5513  opelxp  5657  opthprc  5685  relsnb  5748  relop  5796  issetid  5800  xpid11  5878  elinxp  5975  eldmeldmressn  5981  iss  5991  iresn0n0  6010  asymref2  6071  xpnz  6114  xpdifid  6123  ssrnres  6133  dfrel2  6144  resssxp  6225  relrelss  6228  unixp0  6238  reuop  6248  dfpo2  6251  fn0  6620  funssxp  6687  f00  6713  f0bi  6714  dffo2  6747  f1o00  6806  fo00  6807  fv3  6849  dffn5  6889  dff2  7041  dff3  7042  dffo4  7045  dffo5  7046  exfo  7047  fmpt  7052  fompt  7060  ffnfv  7061  fsn  7077  fsn2  7078  funop  7091  funsneqopb  7094  fnsnbOLD  7109  isores1  7277  ssoprab2b  7424  eqoprab2bw  7425  eqfnov2  7485  unexb  7689  unexbOLD  7690  uniexb  7706  pwexb  7708  iunpw  7713  ordeleqon  7724  dford5  7726  onintrab  7738  ordsuc  7753  unon  7770  onuninsuci  7779  ordzsl  7784  onzsl  7785  f1oexbi  7867  ffoss  7887  1st2ndb  7970  frxp3  8090  suppssov1  8136  suppssov2  8137  suppssfv  8141  reldmtpos  8173  dfrecs3  8301  omopthi  8585  brinxper  8660  ecopover  8754  fsetexb  8797  mapsncnv  8827  mptelixpg  8869  elixpsn  8871  ixpsnf1o  8872  bren2  8916  en0  8951  en0ALT  8952  en0r  8953  en1  8957  en1b  8958  sbthb  9022  dom0  9029  canth2  9054  onfin2  9136  sdom1  9145  1sdom2dom  9149  fineqv  9162  unfilem1  9200  unfib  9204  pwfir  9212  pwfi  9214  fiint  9222  residfi  9233  unifpw  9250  wofib  9442  sucprcreg  9501  opthreg  9519  suc11reg  9520  infeq5  9538  rankwflemb  9697  r1elss  9710  pwwf  9711  unwf  9714  uniwf  9723  rankonid  9733  rankr1id  9766  rankuni  9767  rankxplim3  9785  scott0  9790  karden  9799  djuexb  9813  isnum3  9858  oncard  9864  card1  9872  cardlim  9876  cardmin2  9903  pm54.43lem  9904  ween  9937  acnnum  9954  alephsuc2  9982  alephgeom  9984  iscard3  9995  dfac3  10023  dfac4  10024  dfac5lem3  10027  dfac5  10031  dfac2  10034  dfac8  10038  dfac9  10039  dfacacn  10044  dfac13  10045  dfac12r  10049  dfac12k  10050  kmlem2  10054  kmlem13  10065  djuinf  10091  ackbij2  10144  cflim2  10165  isfin4-2  10216  isfin4p1  10217  isf33lem  10268  compsscnv  10273  fin1a2lem6  10307  domtriom  10345  ac9  10385  ac9s  10395  fodomb  10428  brdom3  10430  brdom5  10431  brdom4  10432  brdom7disj  10433  brdom6disj  10434  iunfo  10441  sdomsdomcard  10462  gch2  10577  gch3  10578  eltsk2g  10653  grutsk  10724  ordpipq  10844  ltbtwnnq  10880  mappsrpr  11010  map2psrpr  11012  elreal2  11034  le2tri3i  11254  elnn0nn  12434  elnnnn0b  12436  elnnnn0c  12437  elnnz  12489  elnn0z  12492  elz2  12497  elnnz1  12508  eluz2b2  12825  elnn1uz2  12829  elpqb  12880  elioo4g  13313  eluzfz2b  13440  fzn0  13445  elfz1end  13461  fzass4  13469  elfz1b  13500  nn0fz0  13532  fzolb  13572  fzon0  13584  elfzo0  13607  elfzo0z  13608  elfzo1  13619  fzo1fzo0n0  13622  om2uzrani  13866  nn0opthi  14184  hashkf  14246  isfinite4  14276  hashprb  14311  hashf1  14371  elss2prb  14402  iswrdb  14434  wrdexb  14439  0wrd0  14454  wrdl3s3  14876  cotr2g  14890  trclun  14928  rexanuz  15260  rexuz3  15263  fsum0diag  15691  fprod0diag  15900  divalgmod  16324  sadcp1  16373  isprm6  16632  nnoddn2prmb  16732  4sqlem4  16871  fnpr2ob  17470  mreunirn  17511  isdrs2  18220  isacs5  18462  isacs4  18463  isacs3  18464  dfgrp2  18883  dfgrp3  18960  dfgrp3e  18961  isnsg3  19080  gicer  19197  oppgmndb  19275  oppggrpb  19278  pmtrfb  19385  invghm  19753  isringrng  20213  opprrngb  20273  opprringb  20275  isnzr2hash  20443  isdomn4  20640  abvn0b  20760  gzrngunit  21379  dvdsrzring  21407  zringunit  21412  zlmlmod  21468  cygth  21517  frgpcyg  21519  zlmassa  21850  toprntopon  22860  tgclb  22905  iscldtop  23030  isnrm2  23293  isnrm3  23294  discmp  23333  dfconn2  23354  2ndcsb  23384  dis2ndc  23395  loclly  23422  unisngl  23462  locfindis  23465  iskgen2  23483  dfac14  23553  kqtop  23680  kqt0  23681  kqreg  23686  kqnrm  23687  hmpher  23719  hmphsymb  23721  hmph0  23730  kqhmph  23754  ist1-5lem  23755  elmptrab2  23763  isfil2  23791  filunirn  23817  isufil2  23843  hausflim  23916  isfcls  23944  alexsubALT  23986  istgp2  24026  ustbas  24162  xmetunirn  24272  dscmet  24507  dscopn  24508  isngp4  24547  zcld  24749  zlmclm  25059  iscmet2  25241  iundisj  25496  i1f1lem  25637  fta1b  26124  elply2  26148  elqaa  26277  aannenlem2  26284  wilth  27028  lgsne0  27293  2lgs  27365  2sqlem2  27376  ostth  27597  elno2  27613  bdayfo  27636  elons2  28215  eln0s  28307  elzn0s  28342  eln0zs  28344  elnnzs  28345  remulscllem1  28422  mpteleeOLD  28894  wrdupgr  29084  wrdumgr  29096  umgrislfupgr  29122  uspgrupgrushgr  29178  usgrumgruspgr  29181  usgruspgrb  29182  usgrislfuspgr  29186  uvtx01vtx  29396  pthspthcyc  29802  wwlksnwwlksnon  29914  elwwlks2ons3  29954  clwwlkn1loopb  30044  eclclwwlkn1  30076  upgriseupth  30208  numclwwlkovh  30374  nmlno0lem  30794  isblo3i  30802  blocni  30806  hvsubeq0i  31064  hvaddcani  31066  bcseqi  31121  isch3  31242  norm1exi  31251  hhsssh  31270  shslubi  31386  dfch2  31408  pjoc1i  31432  pjchi  31433  shs00i  31451  chsscon3i  31462  chlejb1i  31477  chj00i  31488  shjshseli  31494  h1de2ctlem  31556  spanunsni  31580  cmcmi  31593  cmbr3i  31601  cmbr4i  31602  pj11i  31712  hosubeq0i  31827  dmadjrnb  31907  nmlnop0iALT  31996  lnopeq0i  32008  elunop2  32014  lnconi  32034  lncnopbd  32038  adjbdlnb  32085  adjbd1o  32086  adjeq0  32092  rnbra  32108  pjss1coi  32164  pjss2coi  32165  pjnormssi  32169  pjssdif2i  32175  pjssdif1i  32176  dfpjop  32183  pjinvari  32192  pjin2i  32194  pjci  32201  pjcmul1i  32202  pjcmul2i  32203  strb  32259  hstrbi  32267  mdsl1i  32322  atom1d  32354  chrelat2i  32366  cvbr4i  32368  cvexchi  32370  sumdmdi  32421  dmdbr4ati  32422  dmdbr5ati  32423  dmdbr6ati  32424  dmdbr7ati  32425  cdj3i  32442  eqtrb  32474  difeq  32519  iundisjf  32590  fpwrelmap  32740  iundisjfi  32804  xrge0tsmsbi  33084  dfufd2  33559  ccfldextdgrr  33757  issgon  34208  measbasedom  34287  oddpwdc  34439  eulerpartlemt  34456  ballotlem2  34574  ballotlemrinv  34619  bnj1533  34936  bnj983  35035  r1omhf  35189  r1omhfb  35195  r1omhfbregs  35205  fineqvr1ombregs  35207  fineqvnttrclse  35216  0nn0m1nnn0  35229  lfuhgr3  35236  spthcycl  35245  satfv1  35479  satf0op  35493  fmla0xp  35499  fmla1  35503  elmsta  35664  antnestlaw1  35807  antnestlaw2  35808  antnestlaw3  35809  nepss  35834  dfon2  35906  distel  35917  fnimage  36043  altopthsn  36077  ellines  36268  rankeq1o  36287  opnrebl2  36437  df3nandALT1  36515  bj-animbi  36675  bj-dfbi6  36691  bj-consensus  36694  bj-falor2  36701  bj-bibibi  36702  bj-andnotim  36704  bj-cbval  36765  bj-cbvex  36766  bj-ssbeq  36770  bj-19.41al  36776  bj-subst  36778  bj-eqs  36792  bj-cbvexw  36793  bj-sb  36804  bj-substax12  36838  bj-dfnnf3  36874  bj-equs45fv  36928  bj-hbaeb2  36935  bj-hbnaeb  36937  bj-equsal  36943  bj-sbsb  36954  bj-moeub  36966  bj-csbsnlem  37020  bj-snsetex  37080  bj-snglex  37090  bj-1uplth  37124  bj-1uplex  37125  bj-2uplth  37138  bj-2uplex  37139  bj-bm1.3ii  37181  bj-restpw  37209  bj-restuni  37214  bj-discrmoore  37228  bj-snmooreb  37231  bj-elid6  37287  bj-eldiag2  37294  mptsnunlem  37455  topdifinf  37466  elxp8  37488  finxp1o  37509  wl-moae  37633  wl-exeq  37651  wl-aleq  37652  wl-nfeqfb  37653  volsupnfl  37778  cover2  37828  isbnd3  37897  cntotbnd  37909  heibor  37934  isfld2  38118  isfldidl  38181  orfa  38195  eqbrb  38347  eqelb  38349  iss2  38449  issetssr  38668  n0el3  38822  detlem  38954  petlem  38983  prtlem16  39041  isltrn2N  40292  aks6d1c2p2  42285  aks6d1c6isolem3  42342  sn-iotalem  42392  dffltz  42792  eu6w  42834  3cubes  42847  ismrc  42858  isnacs3  42867  rexzrexnn0  42961  eldioph4b  42968  dford3  43185  wopprc  43187  ttac  43193  pw2f1ocnv  43194  dfac11  43219  dfac21  43223  isnumbasabl  43263  isnumbasgrp  43264  dfacbasgrp  43265  aaitgo  43319  dflim5  43486  nvocnvb  43579  dfno2  43585  ifpbi1b  43660  rp-fakeimass  43669  rp-fakeanorass  43670  rp-isfinite5  43674  rp-isfinite6  43675  dfsucon  43680  snen1g  43681  iscard4  43690  rtrclex  43774  cnvtrrel  43827  frege54cor0a  44020  isotone1  44205  isotone2  44206  gneispace  44291  k0004lem3  44306  grumnueq  44444  ismnushort  44458  nanorxor  44462  nzss  44474  pm10.55  44526  pm11.57  44546  pm13.192  44567  pm13.194  44569  ipo0  44605  ifr0  44606  xpexb  44610  3impexpbicom  44637  com3rgbi  44671  pm2.43bgbi  44674  pm2.43cbi  44675  sb5ALT  44682  trsbc  44697  2pm13.193  44709  ax6e2ndeq  44716  2uasbanh  44718  eelT01  44867  eel0T1  44868  uunT1  44936  zfregs2VD  44997  equncomVD  45024  trsbcVD  45033  undif3VD  45038  2pm13.193VD  45059  ax6e2eqVD  45063  ax6e2ndeqVD  45065  2uasbanhVD  45067  ax6e2ndeqALT  45087  tcfr  45120  mptssid  45401  elfzfzo  45441  allbutfi  45553  uzn0bi  45619  dvnprodlem3  46108  elaa2  46394  sge00  46536  elhoi  46702  ovn0  46726  ovolval4lem2  46810  confun  47101  afvfv0bi  47314  ffnafv  47333  afv2ndefb  47386  dfatafv2rnb  47389  afv2fv0b  47428  prpair  47663  sbcpr  47683  fpprel2  47903  sbgoldbmb  47948  vopnbgrelself  48017  isgrtri  48105  stgr1  48123  mgm2mgm  48389  nnpw2pb  48749  0aryfvalel  48796  mo0sn  48977  resinsnlem  49032  homf0  49170  isoval2  49196  oppccicb  49212  oppcciceq  49213  funcf2lem2  49243  initc  49252  isinito2  49660  isinito3  49661  termc  49680  dftermc3  49692  elsetrecs  49861  elpg  49875