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  3497  gencbvex  3507  gencbvex2  3508  pm13.183  3632  rr19.3v  3633  rr19.28v  3634  euxfr2w  3691  euxfr2  3693  reu6  3697  reu3  3698  reuan  3859  dfss2  3932  sspss  4065  complss  4114  unineq  4251  uneqin  4252  difrab  4281  ab0w  4342  sbnfc2  4402  un00  4408  disj  4413  ssdifeq0  4450  r19.2zb  4459  ralidmw  4471  ralidm  4475  ralf0  4477  pwidb  4584  snidb  4625  rabsnifsb  4686  tppreqb  4769  difsnb  4770  pwpw0  4777  sssn  4790  preq12b  4814  unissint  4936  uniintsn  4949  iununi  5063  al0ssb  5263  intex  5299  intnex  5300  axpweq  5306  iin0  5317  nfcvb  5331  eusvnfb  5348  eusv2nf  5350  ralxfrALT  5370  sspwb  5409  unipw  5410  opnz  5433  opth  5436  sbcop1  5448  opeqsng  5463  propeqop  5467  opthwiener  5474  opthhausdorff  5477  opthhausdorff0  5478  rexopabb  5488  ssopab2bw  5507  ssopab2b  5509  pwssun  5530  opelxp  5674  opthprc  5702  relsnb  5765  relop  5814  issetid  5818  xpid11  5896  elinxp  5990  eldmeldmressn  5996  iss  6006  iresn0n0  6025  asymref2  6090  xpnz  6132  xpdifid  6141  ssrnres  6151  dfrel2  6162  resssxp  6243  relrelss  6246  unixp0  6256  reuop  6266  dfpo2  6269  fn0  6649  funssxp  6716  f00  6742  f0bi  6743  dffo2  6776  f1o00  6835  fo00  6836  fv3  6876  dffn5  6919  dff2  7071  dff3  7072  dffo4  7075  dffo5  7076  exfo  7077  fmpt  7082  fompt  7090  ffnfv  7091  fsn  7107  fsn2  7108  funop  7121  funsneqopb  7124  fnsnbOLD  7140  isores1  7309  ssoprab2b  7458  eqoprab2bw  7459  eqfnov2  7519  unexb  7723  unexbOLD  7724  uniexb  7740  pwexb  7742  iunpw  7747  ordeleqon  7758  dford5  7760  onintrab  7772  ordsuc  7788  unon  7806  onuninsuci  7816  ordzsl  7821  onzsl  7822  f1oexbi  7904  ffoss  7924  1st2ndb  8008  frxp3  8130  suppssov1  8176  suppssov2  8177  suppssfv  8181  reldmtpos  8213  dfrecs3  8341  omopthi  8625  brinxper  8700  ecopover  8794  fsetexb  8837  mapsncnv  8866  mptelixpg  8908  elixpsn  8910  ixpsnf1o  8911  bren2  8954  en0  8989  en0ALT  8990  en0r  8991  en1  8995  en1b  8996  sbthb  9062  dom0  9069  canth2  9094  onfin2  9180  sdom1  9189  sdom1OLD  9190  1sdom2dom  9194  1sdomOLD  9196  fineqv  9210  unfilem1  9254  unfib  9258  pwfir  9266  pwfi  9268  fiint  9277  fiintOLD  9278  residfi  9289  unifpw  9306  wofib  9498  sucprcreg  9554  opthreg  9571  suc11reg  9572  infeq5  9590  rankwflemb  9746  r1elss  9759  pwwf  9760  unwf  9763  uniwf  9772  rankonid  9782  rankr1id  9815  rankuni  9816  rankxplim3  9834  scott0  9839  karden  9848  djuexb  9862  isnum3  9907  oncard  9913  card1  9921  cardlim  9925  cardmin2  9952  pm54.43lem  9953  ween  9988  acnnum  10005  alephsuc2  10033  alephgeom  10035  iscard3  10046  dfac3  10074  dfac4  10075  dfac5lem3  10078  dfac5  10082  dfac2  10085  dfac8  10089  dfac9  10090  dfacacn  10095  dfac13  10096  dfac12r  10100  dfac12k  10101  kmlem2  10105  kmlem13  10116  djuinf  10142  ackbij2  10195  cflim2  10216  isfin4-2  10267  isfin4p1  10268  isf33lem  10319  compsscnv  10324  fin1a2lem6  10358  domtriom  10396  ac9  10436  ac9s  10446  fodomb  10479  brdom3  10481  brdom5  10482  brdom4  10483  brdom7disj  10484  brdom6disj  10485  iunfo  10492  sdomsdomcard  10513  gch2  10628  gch3  10629  eltsk2g  10704  grutsk  10775  ordpipq  10895  ltbtwnnq  10931  mappsrpr  11061  map2psrpr  11063  elreal2  11085  le2tri3i  11304  elnn0nn  12484  elnnnn0b  12486  elnnnn0c  12487  elnnz  12539  elnn0z  12542  elz2  12547  elnnz1  12559  eluz2b2  12880  elnn1uz2  12884  elpqb  12935  elioo4g  13367  eluzfz2b  13494  fzn0  13499  elfz1end  13515  fzass4  13523  elfz1b  13554  nn0fz0  13586  fzolb  13626  fzon0  13638  elfzo0  13661  elfzo0z  13662  elfzo1  13673  fzo1fzo0n0  13676  om2uzrani  13917  nn0opthi  14235  hashkf  14297  isfinite4  14327  hashprb  14362  hashf1  14422  elss2prb  14453  iswrdb  14485  wrdexb  14490  0wrd0  14505  wrdl3s3  14928  cotr2g  14942  trclun  14980  rexanuz  15312  rexuz3  15315  fsum0diag  15743  fprod0diag  15952  divalgmod  16376  sadcp1  16425  isprm6  16684  nnoddn2prmb  16784  4sqlem4  16923  fnpr2ob  17521  mreunirn  17562  isdrs2  18267  isacs5  18507  isacs4  18508  isacs3  18509  dfgrp2  18894  dfgrp3  18971  dfgrp3e  18972  isnsg3  19092  gicer  19209  oppgmndb  19287  oppggrpb  19290  pmtrfb  19395  invghm  19763  isringrng  20196  opprrngb  20255  opprringb  20257  isnzr2hash  20428  isdomn4  20625  abvn0b  20745  gzrngunit  21350  dvdsrzring  21371  zringunit  21376  zlmlmod  21432  cygth  21481  frgpcyg  21483  zlmassa  21812  toprntopon  22812  tgclb  22857  iscldtop  22982  isnrm2  23245  isnrm3  23246  discmp  23285  dfconn2  23306  2ndcsb  23336  dis2ndc  23347  loclly  23374  unisngl  23414  locfindis  23417  iskgen2  23435  dfac14  23505  kqtop  23632  kqt0  23633  kqreg  23638  kqnrm  23639  hmpher  23671  hmphsymb  23673  hmph0  23682  kqhmph  23706  ist1-5lem  23707  elmptrab2  23715  isfil2  23743  filunirn  23769  isufil2  23795  hausflim  23868  isfcls  23896  alexsubALT  23938  istgp2  23978  ustbas  24115  xmetunirn  24225  dscmet  24460  dscopn  24461  isngp4  24500  zcld  24702  zlmclm  25012  iscmet2  25194  iundisj  25449  i1f1lem  25590  fta1b  26077  elply2  26101  elqaa  26230  aannenlem2  26237  wilth  26981  lgsne0  27246  2lgs  27318  2sqlem2  27329  ostth  27550  elno2  27566  bdayfo  27589  elons2  28159  eln0s  28251  elzn0s  28286  eln0zs  28288  elnnzs  28289  remulscllem1  28351  mptelee  28822  wrdupgr  29012  wrdumgr  29024  umgrislfupgr  29050  uspgrupgrushgr  29106  usgrumgruspgr  29109  usgruspgrb  29110  usgrislfuspgr  29114  uvtx01vtx  29324  pthspthcyc  29733  wwlksnwwlksnon  29845  elwwlks2ons3  29885  clwwlkn1loopb  29972  eclclwwlkn1  30004  upgriseupth  30136  numclwwlkovh  30302  nmlno0lem  30722  isblo3i  30730  blocni  30734  hvsubeq0i  30992  hvaddcani  30994  bcseqi  31049  isch3  31170  norm1exi  31179  hhsssh  31198  shslubi  31314  dfch2  31336  pjoc1i  31360  pjchi  31361  shs00i  31379  chsscon3i  31390  chlejb1i  31405  chj00i  31416  shjshseli  31422  h1de2ctlem  31484  spanunsni  31508  cmcmi  31521  cmbr3i  31529  cmbr4i  31530  pj11i  31640  hosubeq0i  31755  dmadjrnb  31835  nmlnop0iALT  31924  lnopeq0i  31936  elunop2  31942  lnconi  31962  lncnopbd  31966  adjbdlnb  32013  adjbd1o  32014  adjeq0  32020  rnbra  32036  pjss1coi  32092  pjss2coi  32093  pjnormssi  32097  pjssdif2i  32103  pjssdif1i  32104  dfpjop  32111  pjinvari  32120  pjin2i  32122  pjci  32129  pjcmul1i  32130  pjcmul2i  32131  strb  32187  hstrbi  32195  mdsl1i  32250  atom1d  32282  chrelat2i  32294  cvbr4i  32296  cvexchi  32298  sumdmdi  32349  dmdbr4ati  32350  dmdbr5ati  32351  dmdbr6ati  32352  dmdbr7ati  32353  cdj3i  32370  eqtrb  32403  difeq  32447  iundisjf  32518  fpwrelmap  32656  iundisjfi  32719  xrge0tsmsbi  33003  dfufd2  33521  ccfldextdgrr  33667  issgon  34113  measbasedom  34192  oddpwdc  34345  eulerpartlemt  34362  ballotlem2  34480  ballotlemrinv  34525  bnj1533  34842  bnj983  34941  0nn0m1nnn0  35100  lfuhgr3  35107  spthcycl  35116  satfv1  35350  satf0op  35364  fmla0xp  35370  fmla1  35374  elmsta  35535  antnestlaw1  35678  antnestlaw2  35679  antnestlaw3  35680  nepss  35705  dfon2  35780  distel  35791  fnimage  35917  altopthsn  35949  ellines  36140  rankeq1o  36159  opnrebl2  36309  df3nandALT1  36387  bj-animbi  36547  bj-dfbi6  36563  bj-consensus  36566  bj-falor2  36573  bj-bibibi  36574  bj-andnotim  36576  bj-cbval  36637  bj-cbvex  36638  bj-ssbeq  36641  bj-19.41al  36647  bj-subst  36649  bj-eqs  36663  bj-cbvexw  36664  bj-sb  36675  bj-substax12  36709  bj-dfnnf3  36745  bj-equs45fv  36799  bj-hbaeb2  36806  bj-hbnaeb  36808  bj-equsal  36814  bj-sbsb  36825  bj-moeub  36837  bj-csbsnlem  36891  bj-snsetex  36951  bj-snglex  36961  bj-1uplth  36995  bj-1uplex  36996  bj-2uplth  37009  bj-2uplex  37010  bj-bm1.3ii  37052  bj-restpw  37080  bj-restuni  37085  bj-discrmoore  37099  bj-snmooreb  37102  bj-elid6  37158  bj-eldiag2  37165  mptsnunlem  37326  topdifinf  37337  elxp8  37359  finxp1o  37380  wl-moae  37504  wl-exeq  37522  wl-aleq  37523  wl-nfeqfb  37524  wl-ax11-lem6  37578  volsupnfl  37659  cover2  37709  isbnd3  37778  cntotbnd  37790  heibor  37815  isfld2  37999  isfldidl  38062  orfa  38076  eqbrb  38221  eqelb  38223  iss2  38326  issetssr  38494  n0el3  38643  detlem  38775  petlem  38804  prtlem16  38862  isltrn2N  40114  aks6d1c2p2  42107  aks6d1c6isolem3  42164  sn-iotalem  42209  dffltz  42622  eu6w  42664  3cubes  42678  ismrc  42689  isnacs3  42698  rexzrexnn0  42792  eldioph4b  42799  dford3  43017  wopprc  43019  ttac  43025  pw2f1ocnv  43026  dfac11  43051  dfac21  43055  isnumbasabl  43095  isnumbasgrp  43096  dfacbasgrp  43097  aaitgo  43151  dflim5  43318  nvocnvb  43411  dfno2  43417  ifpbi1b  43492  rp-fakeimass  43501  rp-fakeanorass  43502  rp-isfinite5  43506  rp-isfinite6  43507  dfsucon  43512  snen1g  43513  iscard4  43522  rtrclex  43606  cnvtrrel  43659  frege54cor0a  43852  isotone1  44037  isotone2  44038  gneispace  44123  k0004lem3  44138  grumnueq  44276  ismnushort  44290  nanorxor  44294  nzss  44306  pm10.55  44358  pm11.57  44378  pm13.192  44399  pm13.194  44401  ipo0  44438  ifr0  44439  xpexb  44443  3impexpbicom  44470  com3rgbi  44504  pm2.43bgbi  44507  pm2.43cbi  44508  sb5ALT  44515  trsbc  44530  2pm13.193  44542  ax6e2ndeq  44549  2uasbanh  44551  eelT01  44700  eel0T1  44701  uunT1  44769  zfregs2VD  44830  equncomVD  44857  trsbcVD  44866  undif3VD  44871  2pm13.193VD  44892  ax6e2eqVD  44896  ax6e2ndeqVD  44898  2uasbanhVD  44900  ax6e2ndeqALT  44920  tcfr  44953  mptssid  45235  elfzfzo  45275  allbutfi  45389  uzn0bi  45455  dvnprodlem3  45946  elaa2  46232  sge00  46374  elhoi  46540  ovn0  46564  ovolval4lem2  46648  confun  46940  afvfv0bi  47153  ffnafv  47172  afv2ndefb  47225  dfatafv2rnb  47228  afv2fv0b  47267  prpair  47502  sbcpr  47522  fpprel2  47742  sbgoldbmb  47787  vopnbgrelself  47855  isgrtri  47942  stgr1  47960  mgm2mgm  48215  nnpw2pb  48576  0aryfvalel  48623  mo0sn  48804  resinsnlem  48859  homf0  48998  isoval2  49024  oppccicb  49040  oppcciceq  49041  funcf2lem2  49071  initc  49080  isinito2  49488  isinito3  49489  termc  49508  dftermc3  49520  elsetrecs  49689  elpg  49703