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  r19.35  3087  r19.26  3089  r19.21v  3154  ceqsexOLD  3486  gencbvex  3496  gencbvex2  3497  pm13.183  3621  rr19.3v  3622  rr19.28v  3623  euxfr2w  3680  euxfr2  3682  reu6  3686  reu3  3687  reuan  3848  dfss2  3921  sspss  4053  complss  4102  unineq  4239  uneqin  4240  difrab  4269  ab0w  4330  sbnfc2  4390  un00  4396  disj  4401  ssdifeq0  4438  r19.2zb  4447  ralidmw  4459  ralidm  4463  ralf0  4465  pwidb  4572  snidb  4613  rabsnifsb  4674  tppreqb  4756  difsnb  4757  pwpw0  4764  sssn  4777  preq12b  4801  unissint  4922  uniintsn  4935  iununi  5048  al0ssb  5247  intex  5283  intnex  5284  axpweq  5290  iin0  5301  nfcvb  5315  eusvnfb  5332  eusv2nf  5334  ralxfrALT  5354  sspwb  5392  unipw  5393  opnz  5416  opth  5419  sbcop1  5431  opeqsng  5446  propeqop  5450  opthwiener  5457  opthhausdorff  5460  opthhausdorff0  5461  rexopabb  5471  ssopab2bw  5490  ssopab2b  5492  pwssun  5511  opelxp  5655  opthprc  5683  relsnb  5745  relop  5793  issetid  5797  xpid11  5874  elinxp  5970  eldmeldmressn  5976  iss  5986  iresn0n0  6005  asymref2  6066  xpnz  6108  xpdifid  6117  ssrnres  6127  dfrel2  6138  resssxp  6218  relrelss  6221  unixp0  6231  reuop  6241  dfpo2  6244  fn0  6613  funssxp  6680  f00  6706  f0bi  6707  dffo2  6740  f1o00  6799  fo00  6800  fv3  6840  dffn5  6881  dff2  7033  dff3  7034  dffo4  7037  dffo5  7038  exfo  7039  fmpt  7044  fompt  7052  ffnfv  7053  fsn  7069  fsn2  7070  funop  7083  funsneqopb  7086  fnsnbOLD  7102  isores1  7271  ssoprab2b  7418  eqoprab2bw  7419  eqfnov2  7479  unexb  7683  unexbOLD  7684  uniexb  7700  pwexb  7702  iunpw  7707  ordeleqon  7718  dford5  7720  onintrab  7732  ordsuc  7747  unon  7764  onuninsuci  7773  ordzsl  7778  onzsl  7779  f1oexbi  7861  ffoss  7881  1st2ndb  7964  frxp3  8084  suppssov1  8130  suppssov2  8131  suppssfv  8135  reldmtpos  8167  dfrecs3  8295  omopthi  8579  brinxper  8654  ecopover  8748  fsetexb  8791  mapsncnv  8820  mptelixpg  8862  elixpsn  8864  ixpsnf1o  8865  bren2  8908  en0  8943  en0ALT  8944  en0r  8945  en1  8949  en1b  8950  sbthb  9015  dom0  9022  canth2  9047  onfin2  9130  sdom1  9139  1sdom2dom  9143  fineqv  9156  unfilem1  9194  unfib  9198  pwfir  9206  pwfi  9208  fiint  9216  fiintOLD  9217  residfi  9228  unifpw  9245  wofib  9437  sucprcreg  9496  opthreg  9514  suc11reg  9515  infeq5  9533  rankwflemb  9689  r1elss  9702  pwwf  9703  unwf  9706  uniwf  9715  rankonid  9725  rankr1id  9758  rankuni  9759  rankxplim3  9777  scott0  9782  karden  9791  djuexb  9805  isnum3  9850  oncard  9856  card1  9864  cardlim  9868  cardmin2  9895  pm54.43lem  9896  ween  9929  acnnum  9946  alephsuc2  9974  alephgeom  9976  iscard3  9987  dfac3  10015  dfac4  10016  dfac5lem3  10019  dfac5  10023  dfac2  10026  dfac8  10030  dfac9  10031  dfacacn  10036  dfac13  10037  dfac12r  10041  dfac12k  10042  kmlem2  10046  kmlem13  10057  djuinf  10083  ackbij2  10136  cflim2  10157  isfin4-2  10208  isfin4p1  10209  isf33lem  10260  compsscnv  10265  fin1a2lem6  10299  domtriom  10337  ac9  10377  ac9s  10387  fodomb  10420  brdom3  10422  brdom5  10423  brdom4  10424  brdom7disj  10425  brdom6disj  10426  iunfo  10433  sdomsdomcard  10454  gch2  10569  gch3  10570  eltsk2g  10645  grutsk  10716  ordpipq  10836  ltbtwnnq  10872  mappsrpr  11002  map2psrpr  11004  elreal2  11026  le2tri3i  11246  elnn0nn  12426  elnnnn0b  12428  elnnnn0c  12429  elnnz  12481  elnn0z  12484  elz2  12489  elnnz1  12501  eluz2b2  12822  elnn1uz2  12826  elpqb  12877  elioo4g  13309  eluzfz2b  13436  fzn0  13441  elfz1end  13457  fzass4  13465  elfz1b  13496  nn0fz0  13528  fzolb  13568  fzon0  13580  elfzo0  13603  elfzo0z  13604  elfzo1  13615  fzo1fzo0n0  13618  om2uzrani  13859  nn0opthi  14177  hashkf  14239  isfinite4  14269  hashprb  14304  hashf1  14364  elss2prb  14395  iswrdb  14427  wrdexb  14432  0wrd0  14447  wrdl3s3  14869  cotr2g  14883  trclun  14921  rexanuz  15253  rexuz3  15256  fsum0diag  15684  fprod0diag  15893  divalgmod  16317  sadcp1  16366  isprm6  16625  nnoddn2prmb  16725  4sqlem4  16864  fnpr2ob  17462  mreunirn  17503  isdrs2  18212  isacs5  18454  isacs4  18455  isacs3  18456  dfgrp2  18841  dfgrp3  18918  dfgrp3e  18919  isnsg3  19039  gicer  19156  oppgmndb  19234  oppggrpb  19237  pmtrfb  19344  invghm  19712  isringrng  20172  opprrngb  20231  opprringb  20233  isnzr2hash  20404  isdomn4  20601  abvn0b  20721  gzrngunit  21340  dvdsrzring  21368  zringunit  21373  zlmlmod  21429  cygth  21478  frgpcyg  21480  zlmassa  21810  toprntopon  22810  tgclb  22855  iscldtop  22980  isnrm2  23243  isnrm3  23244  discmp  23283  dfconn2  23304  2ndcsb  23334  dis2ndc  23345  loclly  23372  unisngl  23412  locfindis  23415  iskgen2  23433  dfac14  23503  kqtop  23630  kqt0  23631  kqreg  23636  kqnrm  23637  hmpher  23669  hmphsymb  23671  hmph0  23680  kqhmph  23704  ist1-5lem  23705  elmptrab2  23713  isfil2  23741  filunirn  23767  isufil2  23793  hausflim  23866  isfcls  23894  alexsubALT  23936  istgp2  23976  ustbas  24113  xmetunirn  24223  dscmet  24458  dscopn  24459  isngp4  24498  zcld  24700  zlmclm  25010  iscmet2  25192  iundisj  25447  i1f1lem  25588  fta1b  26075  elply2  26099  elqaa  26228  aannenlem2  26235  wilth  26979  lgsne0  27244  2lgs  27316  2sqlem2  27327  ostth  27548  elno2  27564  bdayfo  27587  elons2  28164  eln0s  28256  elzn0s  28291  eln0zs  28293  elnnzs  28294  remulscllem1  28369  mptelee  28840  wrdupgr  29030  wrdumgr  29042  umgrislfupgr  29068  uspgrupgrushgr  29124  usgrumgruspgr  29127  usgruspgrb  29128  usgrislfuspgr  29132  uvtx01vtx  29342  pthspthcyc  29748  wwlksnwwlksnon  29860  elwwlks2ons3  29900  clwwlkn1loopb  29987  eclclwwlkn1  30019  upgriseupth  30151  numclwwlkovh  30317  nmlno0lem  30737  isblo3i  30745  blocni  30749  hvsubeq0i  31007  hvaddcani  31009  bcseqi  31064  isch3  31185  norm1exi  31194  hhsssh  31213  shslubi  31329  dfch2  31351  pjoc1i  31375  pjchi  31376  shs00i  31394  chsscon3i  31405  chlejb1i  31420  chj00i  31431  shjshseli  31437  h1de2ctlem  31499  spanunsni  31523  cmcmi  31536  cmbr3i  31544  cmbr4i  31545  pj11i  31655  hosubeq0i  31770  dmadjrnb  31850  nmlnop0iALT  31939  lnopeq0i  31951  elunop2  31957  lnconi  31977  lncnopbd  31981  adjbdlnb  32028  adjbd1o  32029  adjeq0  32035  rnbra  32051  pjss1coi  32107  pjss2coi  32108  pjnormssi  32112  pjssdif2i  32118  pjssdif1i  32119  dfpjop  32126  pjinvari  32135  pjin2i  32137  pjci  32144  pjcmul1i  32145  pjcmul2i  32146  strb  32202  hstrbi  32210  mdsl1i  32265  atom1d  32297  chrelat2i  32309  cvbr4i  32311  cvexchi  32313  sumdmdi  32364  dmdbr4ati  32365  dmdbr5ati  32366  dmdbr6ati  32367  dmdbr7ati  32368  cdj3i  32385  eqtrb  32418  difeq  32462  iundisjf  32533  fpwrelmap  32677  iundisjfi  32740  xrge0tsmsbi  33017  dfufd2  33488  ccfldextdgrr  33645  issgon  34096  measbasedom  34175  oddpwdc  34328  eulerpartlemt  34345  ballotlem2  34463  ballotlemrinv  34508  bnj1533  34825  bnj983  34924  fineqvnttrclse  35083  0nn0m1nnn0  35096  lfuhgr3  35103  spthcycl  35112  satfv1  35346  satf0op  35360  fmla0xp  35366  fmla1  35370  elmsta  35531  antnestlaw1  35674  antnestlaw2  35675  antnestlaw3  35676  nepss  35701  dfon2  35776  distel  35787  fnimage  35913  altopthsn  35945  ellines  36136  rankeq1o  36155  opnrebl2  36305  df3nandALT1  36383  bj-animbi  36543  bj-dfbi6  36559  bj-consensus  36562  bj-falor2  36569  bj-bibibi  36570  bj-andnotim  36572  bj-cbval  36633  bj-cbvex  36634  bj-ssbeq  36637  bj-19.41al  36643  bj-subst  36645  bj-eqs  36659  bj-cbvexw  36660  bj-sb  36671  bj-substax12  36705  bj-dfnnf3  36741  bj-equs45fv  36795  bj-hbaeb2  36802  bj-hbnaeb  36804  bj-equsal  36810  bj-sbsb  36821  bj-moeub  36833  bj-csbsnlem  36887  bj-snsetex  36947  bj-snglex  36957  bj-1uplth  36991  bj-1uplex  36992  bj-2uplth  37005  bj-2uplex  37006  bj-bm1.3ii  37048  bj-restpw  37076  bj-restuni  37081  bj-discrmoore  37095  bj-snmooreb  37098  bj-elid6  37154  bj-eldiag2  37161  mptsnunlem  37322  topdifinf  37333  elxp8  37355  finxp1o  37376  wl-moae  37500  wl-exeq  37518  wl-aleq  37519  wl-nfeqfb  37520  wl-ax11-lem6  37574  volsupnfl  37655  cover2  37705  isbnd3  37774  cntotbnd  37786  heibor  37811  isfld2  37995  isfldidl  38058  orfa  38072  eqbrb  38217  eqelb  38219  iss2  38322  issetssr  38490  n0el3  38639  detlem  38771  petlem  38800  prtlem16  38858  isltrn2N  40109  aks6d1c2p2  42102  aks6d1c6isolem3  42159  sn-iotalem  42204  dffltz  42617  eu6w  42659  3cubes  42673  ismrc  42684  isnacs3  42693  rexzrexnn0  42787  eldioph4b  42794  dford3  43011  wopprc  43013  ttac  43019  pw2f1ocnv  43020  dfac11  43045  dfac21  43049  isnumbasabl  43089  isnumbasgrp  43090  dfacbasgrp  43091  aaitgo  43145  dflim5  43312  nvocnvb  43405  dfno2  43411  ifpbi1b  43486  rp-fakeimass  43495  rp-fakeanorass  43496  rp-isfinite5  43500  rp-isfinite6  43501  dfsucon  43506  snen1g  43507  iscard4  43516  rtrclex  43600  cnvtrrel  43653  frege54cor0a  43846  isotone1  44031  isotone2  44032  gneispace  44117  k0004lem3  44132  grumnueq  44270  ismnushort  44284  nanorxor  44288  nzss  44300  pm10.55  44352  pm11.57  44372  pm13.192  44393  pm13.194  44395  ipo0  44432  ifr0  44433  xpexb  44437  3impexpbicom  44464  com3rgbi  44498  pm2.43bgbi  44501  pm2.43cbi  44502  sb5ALT  44509  trsbc  44524  2pm13.193  44536  ax6e2ndeq  44543  2uasbanh  44545  eelT01  44694  eel0T1  44695  uunT1  44763  zfregs2VD  44824  equncomVD  44851  trsbcVD  44860  undif3VD  44865  2pm13.193VD  44886  ax6e2eqVD  44890  ax6e2ndeqVD  44892  2uasbanhVD  44894  ax6e2ndeqALT  44914  tcfr  44947  mptssid  45229  elfzfzo  45269  allbutfi  45382  uzn0bi  45448  dvnprodlem3  45939  elaa2  46225  sge00  46367  elhoi  46533  ovn0  46557  ovolval4lem2  46641  confun  46933  afvfv0bi  47146  ffnafv  47165  afv2ndefb  47218  dfatafv2rnb  47221  afv2fv0b  47260  prpair  47495  sbcpr  47515  fpprel2  47735  sbgoldbmb  47780  vopnbgrelself  47849  isgrtri  47937  stgr1  47955  mgm2mgm  48221  nnpw2pb  48582  0aryfvalel  48629  mo0sn  48810  resinsnlem  48865  homf0  49004  isoval2  49030  oppccicb  49046  oppcciceq  49047  funcf2lem2  49077  initc  49086  isinito2  49494  isinito3  49495  termc  49514  dftermc3  49526  elsetrecs  49695  elpg  49709