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  2209  19.41  2242  sbalex  2249  sbalexOLD  2250  equsexv  2275  sbim  2309  cbvalv1  2345  cbval  2402  equsex  2422  aecom  2431  equs45f  2463  dfsb1  2485  dfsb2  2497  sb6f  2501  dfmoeu  2535  moabs  2543  mo3  2564  mo4  2566  exmoeu  2581  moanimlem  2618  euan  2621  euanv  2624  2mo  2648  2eu6  2657  euae  2660  axextb  2711  eqcom  2743  nebi  3012  r19.35  3094  r19.26  3096  r19.21v  3161  gencbvex  3499  gencbvex2  3500  pm13.183  3620  rr19.3v  3621  rr19.28v  3622  euxfr2w  3678  euxfr2  3680  reu6  3684  reu3  3685  reuan  3846  dfss2  3919  sspss  4054  complss  4103  unineq  4240  uneqin  4241  difrab  4270  sbnfc2  4391  un00  4397  ssdifeq0  4439  r19.2zb  4453  ralidmw  4469  ralidm  4470  pwidb  4575  snidb  4618  rabsnifsb  4679  tppreqb  4761  difsnb  4762  pwpw0  4769  sssn  4782  preq12b  4806  unissint  4927  uniintsn  4940  iununi  5054  al0ssb  5253  intex  5289  intnex  5290  axpweq  5296  iin0  5307  nfcvb  5321  eusvnfb  5338  eusv2nf  5340  ralxfrALT  5360  sspwb  5397  unipw  5398  opnz  5421  opth  5424  sbcop1  5436  opeqsng  5451  propeqop  5455  opthwiener  5462  opthhausdorff  5465  opthhausdorff0  5466  rexopabb  5476  ssopab2bw  5495  ssopab2b  5497  pwssun  5516  opelxp  5660  opthprc  5688  relsnb  5751  relop  5799  issetid  5803  xpid11  5881  elinxp  5978  eldmeldmressn  5984  iss  5994  iresn0n0  6013  asymref2  6074  xpnz  6117  xpdifid  6126  ssrnres  6136  dfrel2  6147  resssxp  6228  relrelss  6231  unixp0  6241  reuop  6251  dfpo2  6254  fn0  6623  funssxp  6690  f00  6716  f0bi  6717  dffo2  6750  f1o00  6809  fo00  6810  fv3  6852  dffn5  6892  dff2  7044  dff3  7045  dffo4  7048  dffo5  7049  exfo  7050  fmpt  7055  fompt  7063  ffnfv  7064  fsn  7080  fsn2  7081  funop  7094  funsneqopb  7097  fnsnbOLD  7112  isores1  7280  ssoprab2b  7427  eqoprab2bw  7428  eqfnov2  7488  unexb  7692  unexbOLD  7693  uniexb  7709  pwexb  7711  iunpw  7716  ordeleqon  7727  dford5  7729  onintrab  7741  ordsuc  7756  unon  7773  onuninsuci  7782  ordzsl  7787  onzsl  7788  f1oexbi  7870  ffoss  7890  1st2ndb  7973  frxp3  8093  suppssov1  8139  suppssov2  8140  suppssfv  8144  reldmtpos  8176  dfrecs3  8304  omopthi  8589  brinxper  8664  ecopover  8758  fsetexb  8801  mapsncnv  8831  mptelixpg  8873  elixpsn  8875  ixpsnf1o  8876  bren2  8920  en0  8955  en0ALT  8956  en0r  8957  en1  8961  en1b  8962  sbthb  9026  dom0  9033  canth2  9058  onfin2  9141  sdom1  9150  1sdom2dom  9154  fineqv  9167  unfilem1  9205  unfib  9209  pwfir  9217  pwfi  9219  fiint  9227  residfi  9238  unifpw  9255  wofib  9450  sucprcreg  9509  opthreg  9527  suc11reg  9528  infeq5  9546  rankwflemb  9705  r1elss  9718  pwwf  9719  unwf  9722  uniwf  9731  rankonid  9741  rankr1id  9774  rankuni  9775  rankxplim3  9793  scott0  9798  karden  9807  djuexb  9821  isnum3  9866  oncard  9872  card1  9880  cardlim  9884  cardmin2  9911  pm54.43lem  9912  ween  9945  acnnum  9962  alephsuc2  9990  alephgeom  9992  iscard3  10003  dfac3  10031  dfac4  10032  dfac5lem3  10035  dfac5  10039  dfac2  10042  dfac8  10046  dfac9  10047  dfacacn  10052  dfac13  10053  dfac12r  10057  dfac12k  10058  kmlem2  10062  kmlem13  10073  djuinf  10099  ackbij2  10152  cflim2  10173  isfin4-2  10224  isfin4p1  10225  isf33lem  10276  compsscnv  10281  fin1a2lem6  10315  domtriom  10353  ac9  10393  ac9s  10403  fodomb  10436  brdom3  10438  brdom5  10439  brdom4  10440  brdom7disj  10441  brdom6disj  10442  iunfo  10449  sdomsdomcard  10470  gch2  10586  gch3  10587  eltsk2g  10662  grutsk  10733  ordpipq  10853  ltbtwnnq  10889  mappsrpr  11019  map2psrpr  11021  elreal2  11043  le2tri3i  11263  elnn0nn  12443  elnnnn0b  12445  elnnnn0c  12446  elnnz  12498  elnn0z  12501  elz2  12506  elnnz1  12517  eluz2b2  12834  elnn1uz2  12838  elpqb  12889  elioo4g  13322  eluzfz2b  13449  fzn0  13454  elfz1end  13470  fzass4  13478  elfz1b  13509  nn0fz0  13541  fzolb  13581  fzon0  13593  elfzo0  13616  elfzo0z  13617  elfzo1  13628  fzo1fzo0n0  13631  om2uzrani  13875  nn0opthi  14193  hashkf  14255  isfinite4  14285  hashprb  14320  hashf1  14380  elss2prb  14411  iswrdb  14443  wrdexb  14448  0wrd0  14463  wrdl3s3  14885  cotr2g  14899  trclun  14937  rexanuz  15269  rexuz3  15272  fsum0diag  15700  fprod0diag  15909  divalgmod  16333  sadcp1  16382  isprm6  16641  nnoddn2prmb  16741  4sqlem4  16880  fnpr2ob  17479  mreunirn  17520  isdrs2  18229  isacs5  18471  isacs4  18472  isacs3  18473  dfgrp2  18892  dfgrp3  18969  dfgrp3e  18970  isnsg3  19089  gicer  19206  oppgmndb  19284  oppggrpb  19287  pmtrfb  19394  invghm  19762  isringrng  20222  opprrngb  20282  opprringb  20284  isnzr2hash  20452  isdomn4  20649  abvn0b  20769  gzrngunit  21388  dvdsrzring  21416  zringunit  21421  zlmlmod  21477  cygth  21526  frgpcyg  21528  zlmassa  21859  toprntopon  22869  tgclb  22914  iscldtop  23039  isnrm2  23302  isnrm3  23303  discmp  23342  dfconn2  23363  2ndcsb  23393  dis2ndc  23404  loclly  23431  unisngl  23471  locfindis  23474  iskgen2  23492  dfac14  23562  kqtop  23689  kqt0  23690  kqreg  23695  kqnrm  23696  hmpher  23728  hmphsymb  23730  hmph0  23739  kqhmph  23763  ist1-5lem  23764  elmptrab2  23772  isfil2  23800  filunirn  23826  isufil2  23852  hausflim  23925  isfcls  23953  alexsubALT  23995  istgp2  24035  ustbas  24171  xmetunirn  24281  dscmet  24516  dscopn  24517  isngp4  24556  zcld  24758  zlmclm  25068  iscmet2  25250  iundisj  25505  i1f1lem  25646  fta1b  26133  elply2  26157  elqaa  26286  aannenlem2  26293  wilth  27037  lgsne0  27302  2lgs  27374  2sqlem2  27385  ostth  27606  elno2  27622  bdayfo  27645  elons2  28254  eln0s2  28353  eln0s  28357  elzn0s  28394  eln0zs  28396  elnnzs  28397  remulscllem1  28496  mpteleeOLD  28968  wrdupgr  29158  wrdumgr  29170  umgrislfupgr  29196  uspgrupgrushgr  29252  usgrumgruspgr  29255  usgruspgrb  29256  usgrislfuspgr  29260  uvtx01vtx  29470  pthspthcyc  29876  wwlksnwwlksnon  29988  elwwlks2ons3  30028  clwwlkn1loopb  30118  eclclwwlkn1  30150  upgriseupth  30282  numclwwlkovh  30448  nmlno0lem  30868  isblo3i  30876  blocni  30880  hvsubeq0i  31138  hvaddcani  31140  bcseqi  31195  isch3  31316  norm1exi  31325  hhsssh  31344  shslubi  31460  dfch2  31482  pjoc1i  31506  pjchi  31507  shs00i  31525  chsscon3i  31536  chlejb1i  31551  chj00i  31562  shjshseli  31568  h1de2ctlem  31630  spanunsni  31654  cmcmi  31667  cmbr3i  31675  cmbr4i  31676  pj11i  31786  hosubeq0i  31901  dmadjrnb  31981  nmlnop0iALT  32070  lnopeq0i  32082  elunop2  32088  lnconi  32108  lncnopbd  32112  adjbdlnb  32159  adjbd1o  32160  adjeq0  32166  rnbra  32182  pjss1coi  32238  pjss2coi  32239  pjnormssi  32243  pjssdif2i  32249  pjssdif1i  32250  dfpjop  32257  pjinvari  32266  pjin2i  32268  pjci  32275  pjcmul1i  32276  pjcmul2i  32277  strb  32333  hstrbi  32341  mdsl1i  32396  atom1d  32428  chrelat2i  32440  cvbr4i  32442  cvexchi  32444  sumdmdi  32495  dmdbr4ati  32496  dmdbr5ati  32497  dmdbr6ati  32498  dmdbr7ati  32499  cdj3i  32516  eqtrb  32548  difeq  32593  iundisjf  32664  fpwrelmap  32812  iundisjfi  32876  xrge0tsmsbi  33156  dfufd2  33631  ccfldextdgrr  33829  issgon  34280  measbasedom  34359  oddpwdc  34511  eulerpartlemt  34528  ballotlem2  34646  ballotlemrinv  34691  bnj1533  35008  bnj983  35107  r1omhf  35262  r1omhfb  35268  fineqvomonb  35275  fineqvnttrclse  35280  r1omhfbregs  35293  fineqvr1ombregs  35294  0nn0m1nnn0  35307  lfuhgr3  35314  spthcycl  35323  satfv1  35557  satf0op  35571  fmla0xp  35577  fmla1  35581  elmsta  35742  antnestlaw1  35885  antnestlaw2  35886  antnestlaw3  35887  nepss  35912  dfon2  35984  distel  35995  fnimage  36121  altopthsn  36155  ellines  36346  rankeq1o  36365  opnrebl2  36515  df3nandALT1  36593  bj-animbi  36759  bj-dfbi6  36775  bj-consensus  36778  bj-falor2  36785  bj-bibibi  36786  bj-andnotim  36788  bj-cbval  36849  bj-cbvex  36850  bj-ssbeq  36854  bj-19.41al  36860  bj-subst  36862  bj-eqs  36876  bj-cbvexw  36877  bj-sb  36888  bj-substax12  36922  bj-dfnnf3  36958  bj-equs45fv  37012  bj-hbaeb2  37019  bj-hbnaeb  37021  bj-equsal  37027  bj-sbsb  37038  bj-moeub  37050  bj-csbsnlem  37104  bj-snsetex  37164  bj-snglex  37174  bj-1uplth  37208  bj-1uplex  37209  bj-2uplth  37222  bj-2uplex  37223  bj-bm1.3ii  37265  bj-restpw  37297  bj-restuni  37302  bj-discrmoore  37316  bj-snmooreb  37319  bj-elid6  37375  bj-eldiag2  37382  mptsnunlem  37543  topdifinf  37554  elxp8  37576  finxp1o  37597  wl-moae  37721  wl-exeq  37739  wl-aleq  37740  wl-nfeqfb  37741  volsupnfl  37866  cover2  37916  isbnd3  37985  cntotbnd  37997  heibor  38022  isfld2  38206  isfldidl  38269  orfa  38283  eqbrb  38435  eqelb  38437  iss2  38537  issetssr  38756  n0el3  38910  detlem  39042  petlem  39071  prtlem16  39129  isltrn2N  40380  aks6d1c2p2  42373  aks6d1c6isolem3  42430  sn-iotalem  42477  dffltz  42877  eu6w  42919  3cubes  42932  ismrc  42943  isnacs3  42952  rexzrexnn0  43046  eldioph4b  43053  dford3  43270  wopprc  43272  ttac  43278  pw2f1ocnv  43279  dfac11  43304  dfac21  43308  isnumbasabl  43348  isnumbasgrp  43349  dfacbasgrp  43350  aaitgo  43404  dflim5  43571  nvocnvb  43663  dfno2  43669  ifpbi1b  43744  rp-fakeimass  43753  rp-fakeanorass  43754  rp-isfinite5  43758  rp-isfinite6  43759  dfsucon  43764  snen1g  43765  iscard4  43774  rtrclex  43858  cnvtrrel  43911  frege54cor0a  44104  isotone1  44289  isotone2  44290  gneispace  44375  k0004lem3  44390  grumnueq  44528  ismnushort  44542  nanorxor  44546  nzss  44558  pm10.55  44610  pm11.57  44630  pm13.192  44651  pm13.194  44653  ipo0  44689  ifr0  44690  xpexb  44694  3impexpbicom  44721  com3rgbi  44755  pm2.43bgbi  44758  pm2.43cbi  44759  sb5ALT  44766  trsbc  44781  2pm13.193  44793  ax6e2ndeq  44800  2uasbanh  44802  eelT01  44951  eel0T1  44952  uunT1  45020  zfregs2VD  45081  equncomVD  45108  trsbcVD  45117  undif3VD  45122  2pm13.193VD  45143  ax6e2eqVD  45147  ax6e2ndeqVD  45149  2uasbanhVD  45151  ax6e2ndeqALT  45171  tcfr  45204  mptssid  45485  elfzfzo  45525  allbutfi  45637  uzn0bi  45703  dvnprodlem3  46192  elaa2  46478  sge00  46620  elhoi  46786  ovn0  46810  ovolval4lem2  46894  confun  47185  afvfv0bi  47398  ffnafv  47417  afv2ndefb  47470  dfatafv2rnb  47473  afv2fv0b  47512  prpair  47747  sbcpr  47767  fpprel2  47987  sbgoldbmb  48032  vopnbgrelself  48101  isgrtri  48189  stgr1  48207  mgm2mgm  48473  nnpw2pb  48833  0aryfvalel  48880  mo0sn  49061  resinsnlem  49116  homf0  49254  isoval2  49280  oppccicb  49296  oppcciceq  49297  funcf2lem2  49327  initc  49336  isinito2  49744  isinito3  49745  termc  49764  dftermc3  49776  elsetrecs  49945  elpg  49959