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  1510  tbw-bijust  1698  tbw-negdf  1699  19.26  1870  19.35  1877  19.21v  1939  19.23v  1942  19.41v  1949  19.3v  1982  19.9v  1984  equcom  2018  cbvalw  2035  alcomw  2045  exexw  2052  sbbii  2077  sban  2081  sbv  2089  alcom  2160  19.3  2203  19.41  2236  sbalex  2243  sbalexOLD  2244  equsexv  2269  sbim  2303  cbvalv1  2339  cbval  2396  equsex  2416  aecom  2425  equs45f  2457  dfsb1  2479  dfsb2  2491  sb6f  2495  dfmoeu  2529  moabs  2536  mobii  2541  mo3  2557  mo4  2559  exmoeu  2574  moanimlem  2611  euan  2614  euanv  2617  2mo  2641  2eu6  2650  euae  2653  axextb  2704  eqcom  2736  nebi  3005  ralcom3OLD  3080  r19.35  3088  r19.35OLD  3089  r19.26  3091  r19.21v  3158  ceqsexOLD  3494  gencbvex  3504  gencbvex2  3505  pm13.183  3629  rr19.3v  3630  rr19.28v  3631  euxfr2w  3688  euxfr2  3690  reu6  3694  reu3  3695  reuan  3856  dfss2  3929  sspss  4061  complss  4110  unineq  4247  uneqin  4248  difrab  4277  ab0w  4338  sbnfc2  4398  un00  4404  disj  4409  ssdifeq0  4446  r19.2zb  4455  ralidmw  4467  ralidm  4471  ralf0  4473  pwidb  4580  snidb  4621  rabsnifsb  4682  tppreqb  4765  difsnb  4766  pwpw0  4773  sssn  4786  preq12b  4810  unissint  4932  uniintsn  4945  iununi  5058  al0ssb  5258  intex  5294  intnex  5295  axpweq  5301  iin0  5312  nfcvb  5326  eusvnfb  5343  eusv2nf  5345  ralxfrALT  5365  sspwb  5404  unipw  5405  opnz  5428  opth  5431  sbcop1  5443  opeqsng  5458  propeqop  5462  opthwiener  5469  opthhausdorff  5472  opthhausdorff0  5473  rexopabb  5483  ssopab2bw  5502  ssopab2b  5504  pwssun  5523  opelxp  5667  opthprc  5695  relsnb  5756  relop  5804  issetid  5808  xpid11  5885  elinxp  5979  eldmeldmressn  5985  iss  5995  iresn0n0  6014  asymref2  6078  xpnz  6120  xpdifid  6129  ssrnres  6139  dfrel2  6150  resssxp  6231  relrelss  6234  unixp0  6244  reuop  6254  dfpo2  6257  fn0  6631  funssxp  6698  f00  6724  f0bi  6725  dffo2  6758  f1o00  6817  fo00  6818  fv3  6858  dffn5  6901  dff2  7053  dff3  7054  dffo4  7057  dffo5  7058  exfo  7059  fmpt  7064  fompt  7072  ffnfv  7073  fsn  7089  fsn2  7090  funop  7103  funsneqopb  7106  fnsnbOLD  7122  isores1  7291  ssoprab2b  7438  eqoprab2bw  7439  eqfnov2  7499  unexb  7703  unexbOLD  7704  uniexb  7720  pwexb  7722  iunpw  7727  ordeleqon  7738  dford5  7740  onintrab  7752  ordsuc  7768  unon  7786  onuninsuci  7796  ordzsl  7801  onzsl  7802  f1oexbi  7884  ffoss  7904  1st2ndb  7987  frxp3  8107  suppssov1  8153  suppssov2  8154  suppssfv  8158  reldmtpos  8190  dfrecs3  8318  omopthi  8602  brinxper  8677  ecopover  8771  fsetexb  8814  mapsncnv  8843  mptelixpg  8885  elixpsn  8887  ixpsnf1o  8888  bren2  8931  en0  8966  en0ALT  8967  en0r  8968  en1  8972  en1b  8973  sbthb  9039  dom0  9046  canth2  9071  onfin2  9157  sdom1  9166  1sdom2dom  9170  1sdomOLD  9172  fineqv  9186  unfilem1  9230  unfib  9234  pwfir  9242  pwfi  9244  fiint  9253  fiintOLD  9254  residfi  9265  unifpw  9282  wofib  9474  sucprcreg  9530  opthreg  9547  suc11reg  9548  infeq5  9566  rankwflemb  9722  r1elss  9735  pwwf  9736  unwf  9739  uniwf  9748  rankonid  9758  rankr1id  9791  rankuni  9792  rankxplim3  9810  scott0  9815  karden  9824  djuexb  9838  isnum3  9883  oncard  9889  card1  9897  cardlim  9901  cardmin2  9928  pm54.43lem  9929  ween  9964  acnnum  9981  alephsuc2  10009  alephgeom  10011  iscard3  10022  dfac3  10050  dfac4  10051  dfac5lem3  10054  dfac5  10058  dfac2  10061  dfac8  10065  dfac9  10066  dfacacn  10071  dfac13  10072  dfac12r  10076  dfac12k  10077  kmlem2  10081  kmlem13  10092  djuinf  10118  ackbij2  10171  cflim2  10192  isfin4-2  10243  isfin4p1  10244  isf33lem  10295  compsscnv  10300  fin1a2lem6  10334  domtriom  10372  ac9  10412  ac9s  10422  fodomb  10455  brdom3  10457  brdom5  10458  brdom4  10459  brdom7disj  10460  brdom6disj  10461  iunfo  10468  sdomsdomcard  10489  gch2  10604  gch3  10605  eltsk2g  10680  grutsk  10751  ordpipq  10871  ltbtwnnq  10907  mappsrpr  11037  map2psrpr  11039  elreal2  11061  le2tri3i  11280  elnn0nn  12460  elnnnn0b  12462  elnnnn0c  12463  elnnz  12515  elnn0z  12518  elz2  12523  elnnz1  12535  eluz2b2  12856  elnn1uz2  12860  elpqb  12911  elioo4g  13343  eluzfz2b  13470  fzn0  13475  elfz1end  13491  fzass4  13499  elfz1b  13530  nn0fz0  13562  fzolb  13602  fzon0  13614  elfzo0  13637  elfzo0z  13638  elfzo1  13649  fzo1fzo0n0  13652  om2uzrani  13893  nn0opthi  14211  hashkf  14273  isfinite4  14303  hashprb  14338  hashf1  14398  elss2prb  14429  iswrdb  14461  wrdexb  14466  0wrd0  14481  wrdl3s3  14904  cotr2g  14918  trclun  14956  rexanuz  15288  rexuz3  15291  fsum0diag  15719  fprod0diag  15928  divalgmod  16352  sadcp1  16401  isprm6  16660  nnoddn2prmb  16760  4sqlem4  16899  fnpr2ob  17497  mreunirn  17538  isdrs2  18243  isacs5  18483  isacs4  18484  isacs3  18485  dfgrp2  18870  dfgrp3  18947  dfgrp3e  18948  isnsg3  19068  gicer  19185  oppgmndb  19263  oppggrpb  19266  pmtrfb  19371  invghm  19739  isringrng  20172  opprrngb  20231  opprringb  20233  isnzr2hash  20404  isdomn4  20601  abvn0b  20721  gzrngunit  21326  dvdsrzring  21347  zringunit  21352  zlmlmod  21408  cygth  21457  frgpcyg  21459  zlmassa  21788  toprntopon  22788  tgclb  22833  iscldtop  22958  isnrm2  23221  isnrm3  23222  discmp  23261  dfconn2  23282  2ndcsb  23312  dis2ndc  23323  loclly  23350  unisngl  23390  locfindis  23393  iskgen2  23411  dfac14  23481  kqtop  23608  kqt0  23609  kqreg  23614  kqnrm  23615  hmpher  23647  hmphsymb  23649  hmph0  23658  kqhmph  23682  ist1-5lem  23683  elmptrab2  23691  isfil2  23719  filunirn  23745  isufil2  23771  hausflim  23844  isfcls  23872  alexsubALT  23914  istgp2  23954  ustbas  24091  xmetunirn  24201  dscmet  24436  dscopn  24437  isngp4  24476  zcld  24678  zlmclm  24988  iscmet2  25170  iundisj  25425  i1f1lem  25566  fta1b  26053  elply2  26077  elqaa  26206  aannenlem2  26213  wilth  26957  lgsne0  27222  2lgs  27294  2sqlem2  27305  ostth  27526  elno2  27542  bdayfo  27565  elons2  28135  eln0s  28227  elzn0s  28262  eln0zs  28264  elnnzs  28265  remulscllem1  28327  mptelee  28798  wrdupgr  28988  wrdumgr  29000  umgrislfupgr  29026  uspgrupgrushgr  29082  usgrumgruspgr  29085  usgruspgrb  29086  usgrislfuspgr  29090  uvtx01vtx  29300  pthspthcyc  29706  wwlksnwwlksnon  29818  elwwlks2ons3  29858  clwwlkn1loopb  29945  eclclwwlkn1  29977  upgriseupth  30109  numclwwlkovh  30275  nmlno0lem  30695  isblo3i  30703  blocni  30707  hvsubeq0i  30965  hvaddcani  30967  bcseqi  31022  isch3  31143  norm1exi  31152  hhsssh  31171  shslubi  31287  dfch2  31309  pjoc1i  31333  pjchi  31334  shs00i  31352  chsscon3i  31363  chlejb1i  31378  chj00i  31389  shjshseli  31395  h1de2ctlem  31457  spanunsni  31481  cmcmi  31494  cmbr3i  31502  cmbr4i  31503  pj11i  31613  hosubeq0i  31728  dmadjrnb  31808  nmlnop0iALT  31897  lnopeq0i  31909  elunop2  31915  lnconi  31935  lncnopbd  31939  adjbdlnb  31986  adjbd1o  31987  adjeq0  31993  rnbra  32009  pjss1coi  32065  pjss2coi  32066  pjnormssi  32070  pjssdif2i  32076  pjssdif1i  32077  dfpjop  32084  pjinvari  32093  pjin2i  32095  pjci  32102  pjcmul1i  32103  pjcmul2i  32104  strb  32160  hstrbi  32168  mdsl1i  32223  atom1d  32255  chrelat2i  32267  cvbr4i  32269  cvexchi  32271  sumdmdi  32322  dmdbr4ati  32323  dmdbr5ati  32324  dmdbr6ati  32325  dmdbr7ati  32326  cdj3i  32343  eqtrb  32376  difeq  32420  iundisjf  32491  fpwrelmap  32629  iundisjfi  32692  xrge0tsmsbi  32976  dfufd2  33494  ccfldextdgrr  33640  issgon  34086  measbasedom  34165  oddpwdc  34318  eulerpartlemt  34335  ballotlem2  34453  ballotlemrinv  34498  bnj1533  34815  bnj983  34914  0nn0m1nnn0  35073  lfuhgr3  35080  spthcycl  35089  satfv1  35323  satf0op  35337  fmla0xp  35343  fmla1  35347  elmsta  35508  antnestlaw1  35651  antnestlaw2  35652  antnestlaw3  35653  nepss  35678  dfon2  35753  distel  35764  fnimage  35890  altopthsn  35922  ellines  36113  rankeq1o  36132  opnrebl2  36282  df3nandALT1  36360  bj-animbi  36520  bj-dfbi6  36536  bj-consensus  36539  bj-falor2  36546  bj-bibibi  36547  bj-andnotim  36549  bj-cbval  36610  bj-cbvex  36611  bj-ssbeq  36614  bj-19.41al  36620  bj-subst  36622  bj-eqs  36636  bj-cbvexw  36637  bj-sb  36648  bj-substax12  36682  bj-dfnnf3  36718  bj-equs45fv  36772  bj-hbaeb2  36779  bj-hbnaeb  36781  bj-equsal  36787  bj-sbsb  36798  bj-moeub  36810  bj-csbsnlem  36864  bj-snsetex  36924  bj-snglex  36934  bj-1uplth  36968  bj-1uplex  36969  bj-2uplth  36982  bj-2uplex  36983  bj-bm1.3ii  37025  bj-restpw  37053  bj-restuni  37058  bj-discrmoore  37072  bj-snmooreb  37075  bj-elid6  37131  bj-eldiag2  37138  mptsnunlem  37299  topdifinf  37310  elxp8  37332  finxp1o  37353  wl-moae  37477  wl-exeq  37495  wl-aleq  37496  wl-nfeqfb  37497  wl-ax11-lem6  37551  volsupnfl  37632  cover2  37682  isbnd3  37751  cntotbnd  37763  heibor  37788  isfld2  37972  isfldidl  38035  orfa  38049  eqbrb  38194  eqelb  38196  iss2  38299  issetssr  38467  n0el3  38616  detlem  38748  petlem  38777  prtlem16  38835  isltrn2N  40087  aks6d1c2p2  42080  aks6d1c6isolem3  42137  sn-iotalem  42182  dffltz  42595  eu6w  42637  3cubes  42651  ismrc  42662  isnacs3  42671  rexzrexnn0  42765  eldioph4b  42772  dford3  42990  wopprc  42992  ttac  42998  pw2f1ocnv  42999  dfac11  43024  dfac21  43028  isnumbasabl  43068  isnumbasgrp  43069  dfacbasgrp  43070  aaitgo  43124  dflim5  43291  nvocnvb  43384  dfno2  43390  ifpbi1b  43465  rp-fakeimass  43474  rp-fakeanorass  43475  rp-isfinite5  43479  rp-isfinite6  43480  dfsucon  43485  snen1g  43486  iscard4  43495  rtrclex  43579  cnvtrrel  43632  frege54cor0a  43825  isotone1  44010  isotone2  44011  gneispace  44096  k0004lem3  44111  grumnueq  44249  ismnushort  44263  nanorxor  44267  nzss  44279  pm10.55  44331  pm11.57  44351  pm13.192  44372  pm13.194  44374  ipo0  44411  ifr0  44412  xpexb  44416  3impexpbicom  44443  com3rgbi  44477  pm2.43bgbi  44480  pm2.43cbi  44481  sb5ALT  44488  trsbc  44503  2pm13.193  44515  ax6e2ndeq  44522  2uasbanh  44524  eelT01  44673  eel0T1  44674  uunT1  44742  zfregs2VD  44803  equncomVD  44830  trsbcVD  44839  undif3VD  44844  2pm13.193VD  44865  ax6e2eqVD  44869  ax6e2ndeqVD  44871  2uasbanhVD  44873  ax6e2ndeqALT  44893  tcfr  44926  mptssid  45208  elfzfzo  45248  allbutfi  45362  uzn0bi  45428  dvnprodlem3  45919  elaa2  46205  sge00  46347  elhoi  46513  ovn0  46537  ovolval4lem2  46621  confun  46913  afvfv0bi  47126  ffnafv  47145  afv2ndefb  47198  dfatafv2rnb  47201  afv2fv0b  47240  prpair  47475  sbcpr  47495  fpprel2  47715  sbgoldbmb  47760  vopnbgrelself  47828  isgrtri  47915  stgr1  47933  mgm2mgm  48188  nnpw2pb  48549  0aryfvalel  48596  mo0sn  48777  resinsnlem  48832  homf0  48971  isoval2  48997  oppccicb  49013  oppcciceq  49014  funcf2lem2  49044  initc  49053  isinito2  49461  isinito3  49462  termc  49481  dftermc3  49493  elsetrecs  49662  elpg  49676