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  829  orcom  871  dfor2  902  oridm  905  orbi2i  913  or12  921  biorfriOLD  941  pm4.72  952  oibabs  954  jaob  964  pm4.44  999  pm4.79  1006  andi  1010  pm4.82  1026  cases2ALT  1049  consensus  1053  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  1981  19.9v  1983  equcom  2017  cbvalw  2034  alcomw  2044  exexw  2051  sbbii  2076  sban  2080  sbv  2088  alcom  2159  19.3  2202  19.41  2235  sbalex  2242  sbalexOLD  2243  equsexv  2268  sbim  2303  cbvalv1  2343  cbval  2403  equsex  2423  aecom  2432  equs45f  2464  dfsb1  2486  dfsb2  2498  sb6f  2502  dfmoeu  2536  moabs  2543  mobii  2548  mo3  2564  mo4  2566  exmoeu  2581  moanimlem  2618  euan  2621  euanv  2624  2mo  2648  2eu6  2657  euae  2660  axextb  2711  eqcom  2744  nebi  3021  ralcom3OLD  3098  r19.35  3108  r19.35OLD  3109  r19.26  3111  r19.21v  3180  ceqsexOLD  3531  gencbvex  3541  gencbvex2  3542  pm13.183  3666  rr19.3v  3667  rr19.28v  3668  euxfr2w  3726  euxfr2  3728  reu6  3732  reu3  3733  reuan  3896  dfss2  3969  sspss  4102  complss  4151  unineq  4288  uneqin  4289  difrab  4318  ab0w  4379  sbnfc2  4439  un00  4445  disj  4450  ssdifeq0  4487  r19.2zb  4496  ralidmw  4508  ralidm  4512  ralf0  4514  pwidb  4621  snidb  4661  rabsnifsb  4722  tppreqb  4805  difsnb  4806  pwpw0  4813  sssn  4826  preq12b  4850  unissint  4972  uniintsn  4985  iununi  5099  al0ssb  5308  intex  5344  intnex  5345  axpweq  5351  iin0  5362  nfcvb  5376  eusvnfb  5393  eusv2nf  5395  ralxfrALT  5415  sspwb  5454  unipw  5455  opnz  5478  opth  5481  sbcop1  5493  opeqsng  5508  propeqop  5512  opthwiener  5519  opthhausdorff  5522  opthhausdorff0  5523  rexopabb  5533  ssopab2bw  5552  ssopab2b  5554  pwssun  5575  opelxp  5721  opthprc  5749  relsnb  5812  relop  5861  issetid  5865  xpid11  5943  elinxp  6037  eldmeldmressn  6043  iss  6053  iresn0n0  6072  asymref2  6137  xpnz  6179  xpdifid  6188  ssrnres  6198  dfrel2  6209  resssxp  6290  relrelss  6293  unixp0  6303  reuop  6313  dfpo2  6316  fn0  6699  funssxp  6764  f00  6790  f0bi  6791  dffo2  6824  f1o00  6883  fo00  6884  fv3  6924  dffn5  6967  dff2  7119  dff3  7120  dffo4  7123  dffo5  7124  exfo  7125  fmpt  7130  fompt  7138  ffnfv  7139  fsn  7155  fsn2  7156  funop  7169  funsneqopb  7172  fnsnb  7186  isores1  7354  ssoprab2b  7502  eqoprab2bw  7503  eqfnov2  7563  unexb  7767  unexbOLD  7768  uniexb  7784  pwexb  7786  iunpw  7791  ordeleqon  7802  dford5  7804  onintrab  7816  ordsuc  7833  unon  7851  onuninsuci  7861  ordzsl  7866  onzsl  7867  f1oexbi  7950  ffoss  7970  1st2ndb  8054  frxp3  8176  suppssov1  8222  suppssov2  8223  suppssfv  8227  reldmtpos  8259  dfrecs3  8412  dfrecs3OLD  8413  omopthi  8699  brinxper  8774  ecopover  8861  fsetexb  8904  mapsncnv  8933  mptelixpg  8975  elixpsn  8977  ixpsnf1o  8978  bren2  9023  en0  9058  en0ALT  9059  en0r  9060  en1  9064  en1b  9065  sbthb  9134  dom0  9142  canth2  9170  onfin2  9268  sdom1  9278  sdom1OLD  9279  1sdom2dom  9283  1sdomOLD  9285  fineqv  9299  unfilem1  9343  unfib  9347  pwfir  9355  pwfi  9357  fiint  9366  fiintOLD  9367  residfi  9378  unifpw  9395  wofib  9585  sucprcreg  9641  opthreg  9658  suc11reg  9659  infeq5  9677  rankwflemb  9833  r1elss  9846  pwwf  9847  unwf  9850  uniwf  9859  rankonid  9869  rankr1id  9902  rankuni  9903  rankxplim3  9921  scott0  9926  karden  9935  djuexb  9949  isnum3  9994  oncard  10000  card1  10008  cardlim  10012  cardmin2  10039  pm54.43lem  10040  ween  10075  acnnum  10092  alephsuc2  10120  alephgeom  10122  iscard3  10133  dfac3  10161  dfac4  10162  dfac5lem3  10165  dfac5  10169  dfac2  10172  dfac8  10176  dfac9  10177  dfacacn  10182  dfac13  10183  dfac12r  10187  dfac12k  10188  kmlem2  10192  kmlem13  10203  djuinf  10229  ackbij2  10282  cflim2  10303  isfin4-2  10354  isfin4p1  10355  isf33lem  10406  compsscnv  10411  fin1a2lem6  10445  domtriom  10483  ac9  10523  ac9s  10533  fodomb  10566  brdom3  10568  brdom5  10569  brdom4  10570  brdom7disj  10571  brdom6disj  10572  iunfo  10579  sdomsdomcard  10600  gch2  10715  gch3  10716  eltsk2g  10791  grutsk  10862  ordpipq  10982  ltbtwnnq  11018  mappsrpr  11148  map2psrpr  11150  elreal2  11172  le2tri3i  11391  elnn0nn  12568  elnnnn0b  12570  elnnnn0c  12571  elnnz  12623  elnn0z  12626  elz2  12631  elnnz1  12643  eluz2b2  12963  elnn1uz2  12967  elpqb  13018  elioo4g  13447  eluzfz2b  13573  fzn0  13578  elfz1end  13594  fzass4  13602  elfz1b  13633  nn0fz0  13665  fzolb  13705  fzon0  13717  elfzo0  13740  elfzo0z  13741  elfzo1  13752  fzo1fzo0n0  13754  om2uzrani  13993  nn0opthi  14309  hashkf  14371  isfinite4  14401  hashprb  14436  hashf1  14496  elss2prb  14527  iswrdb  14558  wrdexb  14563  0wrd0  14578  wrdl3s3  15001  cotr2g  15015  trclun  15053  rexanuz  15384  rexuz3  15387  fsum0diag  15813  fprod0diag  16022  divalgmod  16443  sadcp1  16492  isprm6  16751  nnoddn2prmb  16851  4sqlem4  16990  fnpr2ob  17603  mreunirn  17644  isdrs2  18352  isacs5  18593  isacs4  18594  isacs3  18595  dfgrp2  18980  dfgrp3  19057  dfgrp3e  19058  isnsg3  19178  gicer  19295  oppgmndb  19374  oppggrpb  19377  pmtrfb  19483  invghm  19851  isringrng  20284  opprrngb  20346  opprringb  20348  isnzr2hash  20519  isdomn4  20716  abvn0b  20837  gzrngunit  21451  dvdsrzring  21472  zringunit  21477  zlmlmod  21537  cygth  21590  frgpcyg  21592  zlmassa  21923  toprntopon  22931  tgclb  22977  iscldtop  23103  isnrm2  23366  isnrm3  23367  discmp  23406  dfconn2  23427  2ndcsb  23457  dis2ndc  23468  loclly  23495  unisngl  23535  locfindis  23538  iskgen2  23556  dfac14  23626  kqtop  23753  kqt0  23754  kqreg  23759  kqnrm  23760  hmpher  23792  hmphsymb  23794  hmph0  23803  kqhmph  23827  ist1-5lem  23828  elmptrab2  23836  isfil2  23864  filunirn  23890  isufil2  23916  hausflim  23989  isfcls  24017  alexsubALT  24059  istgp2  24099  ustbas  24236  xmetunirn  24347  dscmet  24585  dscopn  24586  isngp4  24625  zcld  24835  zlmclm  25145  iscmet2  25328  iundisj  25583  i1f1lem  25724  fta1b  26211  elply2  26235  elqaa  26364  aannenlem2  26371  wilth  27114  lgsne0  27379  2lgs  27451  2sqlem2  27462  ostth  27683  elno2  27699  bdayfo  27722  elons2  28281  eln0s  28358  elzn0s  28384  eln0zs  28386  elnnzs  28387  remulscllem1  28432  mptelee  28910  wrdupgr  29102  wrdumgr  29114  umgrislfupgr  29140  uspgrupgrushgr  29196  usgrumgruspgr  29199  usgruspgrb  29200  usgrislfuspgr  29204  uvtx01vtx  29414  pthspthcyc  29823  wwlksnwwlksnon  29935  elwwlks2ons3  29975  clwwlkn1loopb  30062  eclclwwlkn1  30094  upgriseupth  30226  numclwwlkovh  30392  nmlno0lem  30812  isblo3i  30820  blocni  30824  hvsubeq0i  31082  hvaddcani  31084  bcseqi  31139  isch3  31260  norm1exi  31269  hhsssh  31288  shslubi  31404  dfch2  31426  pjoc1i  31450  pjchi  31451  shs00i  31469  chsscon3i  31480  chlejb1i  31495  chj00i  31506  shjshseli  31512  h1de2ctlem  31574  spanunsni  31598  cmcmi  31611  cmbr3i  31619  cmbr4i  31620  pj11i  31730  hosubeq0i  31845  dmadjrnb  31925  nmlnop0iALT  32014  lnopeq0i  32026  elunop2  32032  lnconi  32052  lncnopbd  32056  adjbdlnb  32103  adjbd1o  32104  adjeq0  32110  rnbra  32126  pjss1coi  32182  pjss2coi  32183  pjnormssi  32187  pjssdif2i  32193  pjssdif1i  32194  dfpjop  32201  pjinvari  32210  pjin2i  32212  pjci  32219  pjcmul1i  32220  pjcmul2i  32221  strb  32277  hstrbi  32285  mdsl1i  32340  atom1d  32372  chrelat2i  32384  cvbr4i  32386  cvexchi  32388  sumdmdi  32439  dmdbr4ati  32440  dmdbr5ati  32441  dmdbr6ati  32442  dmdbr7ati  32443  cdj3i  32460  eqtrb  32493  difeq  32537  iundisjf  32602  fpwrelmap  32744  iundisjfi  32798  xrge0tsmsbi  33066  dfufd2  33578  ccfldextdgrr  33722  issgon  34124  measbasedom  34203  oddpwdc  34356  eulerpartlemt  34373  ballotlem2  34491  ballotlemrinv  34536  bnj1533  34866  bnj983  34965  0nn0m1nnn0  35118  lfuhgr3  35125  spthcycl  35134  satfv1  35368  satf0op  35382  fmla0xp  35388  fmla1  35392  elmsta  35553  nepss  35718  dfon2  35793  distel  35804  fnimage  35930  altopthsn  35962  ellines  36153  rankeq1o  36172  opnrebl2  36322  df3nandALT1  36400  bj-animbi  36560  bj-dfbi6  36576  bj-consensus  36579  bj-falor2  36586  bj-bibibi  36587  bj-andnotim  36589  bj-cbval  36650  bj-cbvex  36651  bj-ssbeq  36654  bj-19.41al  36660  bj-subst  36662  bj-eqs  36676  bj-cbvexw  36677  bj-sb  36688  bj-substax12  36722  bj-dfnnf3  36758  bj-equs45fv  36812  bj-hbaeb2  36819  bj-hbnaeb  36821  bj-equsal  36827  bj-sbsb  36838  bj-moeub  36850  bj-csbsnlem  36904  bj-snsetex  36964  bj-snglex  36974  bj-1uplth  37008  bj-1uplex  37009  bj-2uplth  37022  bj-2uplex  37023  bj-bm1.3ii  37065  bj-restpw  37093  bj-restuni  37098  bj-discrmoore  37112  bj-snmooreb  37115  bj-elid6  37171  bj-eldiag2  37178  mptsnunlem  37339  topdifinf  37350  elxp8  37372  finxp1o  37393  wl-moae  37517  wl-exeq  37535  wl-aleq  37536  wl-nfeqfb  37537  wl-ax11-lem6  37591  volsupnfl  37672  cover2  37722  isbnd3  37791  cntotbnd  37803  heibor  37828  isfld2  38012  isfldidl  38075  orfa  38089  eqbrb  38234  eqelb  38236  iss2  38345  issetssr  38504  n0el3  38652  detlem  38784  petlem  38813  prtlem16  38870  isltrn2N  40122  aks6d1c2p2  42120  aks6d1c6isolem3  42177  sn-iotalem  42260  dffltz  42644  eu6w  42686  3cubes  42701  ismrc  42712  isnacs3  42721  rexzrexnn0  42815  eldioph4b  42822  dford3  43040  wopprc  43042  ttac  43048  pw2f1ocnv  43049  dfac11  43074  dfac21  43078  isnumbasabl  43118  isnumbasgrp  43119  dfacbasgrp  43120  aaitgo  43174  dflim5  43342  nvocnvb  43435  dfno2  43441  ifpbi1b  43516  rp-fakeimass  43525  rp-fakeanorass  43526  rp-isfinite5  43530  rp-isfinite6  43531  dfsucon  43536  snen1g  43537  iscard4  43546  rtrclex  43630  cnvtrrel  43683  frege54cor0a  43876  isotone1  44061  isotone2  44062  gneispace  44147  k0004lem3  44162  grumnueq  44306  ismnushort  44320  nanorxor  44324  nzss  44336  pm10.55  44388  pm11.57  44408  pm13.192  44429  pm13.194  44431  ipo0  44468  ifr0  44469  xpexb  44473  3impexpbicom  44500  com3rgbi  44534  pm2.43bgbi  44537  pm2.43cbi  44538  sb5ALT  44545  trsbc  44560  2pm13.193  44572  ax6e2ndeq  44579  2uasbanh  44581  eelT01  44731  eel0T1  44732  uunT1  44800  zfregs2VD  44861  equncomVD  44888  trsbcVD  44897  undif3VD  44902  2pm13.193VD  44923  ax6e2eqVD  44927  ax6e2ndeqVD  44929  2uasbanhVD  44931  ax6e2ndeqALT  44951  tcfr  44980  mptssid  45247  elfzfzo  45288  allbutfi  45404  uzn0bi  45470  dvnprodlem3  45963  elaa2  46249  sge00  46391  elhoi  46557  ovn0  46581  ovolval4lem2  46665  confun  46951  afvfv0bi  47164  ffnafv  47183  afv2ndefb  47236  dfatafv2rnb  47239  afv2fv0b  47278  prpair  47488  sbcpr  47508  fpprel2  47728  sbgoldbmb  47773  vopnbgrelself  47841  isgrtri  47910  stgr1  47928  mgm2mgm  48143  nnpw2pb  48508  0aryfvalel  48555  mo0sn  48735  resinsnlem  48771  funcf2lem2  48915  termc  49149  elsetrecs  49219  elpg  49233