Theorem impbii 212

Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 211. (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 211	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
4	1, 2, 3	mp2 9	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bicom  225  biid  264  2th  267  pm5.74  273  bitri  278  notnotb  318  con34b  319  notbi  322  bibi2i  340  con1b  361  con2b  362  bi2.04  391  imdi  393  pm4.8  397  pm4.81  398  impexp  455  ancom  465  anass  473  jcab  526  abab  839  impimprbi  841  orcom  883  dfor2  914  oridm  917  orbi2i  925  or12  933  biorfriOLD  953  pm4.72  964  oibabs  966  jaob  976  pm4.44  1012  pm4.79  1021  andi  1025  pm4.82  1041  cases2ALT  1064  consensus  1068  3impexp  1377  nanass  1540  tbw-bijust  1728  tbw-negdf  1729  19.26  1900  19.35  1907  19.21v  1969  19.23v  1972  19.41v  1979  19.3v  2012  19.9v  2014  equcom  2048  cbvalw  2065  alcomw  2075  excomw  2076  exexw  2083  sbbii  2110  sban  2114  sbv  2122  sbrimvw  2125  alcom  2194  19.3  2238  19.41  2271  sbalex  2278  sbalexOLD  2279  equsexv  2304  sbim  2338  cbvalv1  2373  cbval  2430  equsex  2450  aecom  2459  equs45f  2491  dfsb1  2513  dfsb2  2525  sb6f  2529  dfmoeu  2563  moabs  2571  mo3  2592  mo4  2594  exmoeu  2609  moanimlem  2646  euan  2649  euanv  2652  2mo  2676  2eu6  2684  euae  2687  axextb  2738  eqcom  2770  nebi  3038  r19.35  3123  r19.26  3125  r19.21v  3190  gencbvex  3511  gencbvex2  3512  pm13.183  3625  rr19.3v  3626  rr19.28v  3627  euxfr2w  3683  euxfr2  3685  reu6  3689  reu3  3690  reuan  3850  dfss2  3923  sspss  4056  complss  4105  unineq  4241  uneqin  4242  difrab  4271  un00  4364  vvin  4366  sbnfc2  4404  ssdifeq0  4447  r19.2zb  4461  ralidmw  4477  ralidm  4478  pwidb  4584  snidb  4627  rabsnifsb  4688  tppreqb  4773  difsnb  4774  pwpw0  4779  sssn  4792  preq12b  4815  unissint  4937  uniintsn  4950  iununi  5065  al0ssb  5271  intex  5314  intnex  5315  axpweq  5321  iin0  5333  nfcvb  5347  eusvnfb  5364  eusv2nf  5366  ralxfrALT  5386  sspwb  5430  unipw  5431  opnz  5455  opth  5458  sbcop1  5470  opeqsng  5486  propeqop  5490  opthwiener  5497  opthhausdorff  5500  opthhausdorff0  5501  rexopabb  5512  ssopab2bw  5532  ssopab2b  5534  pwssun  5553  opelxp  5697  opthprc  5725  relsnb  5789  relop  5836  issetid  5840  xpid11  5922  elinxp  6018  eldmeldmressn  6024  iss  6037  iresn0n0  6056  asymref2  6117  xpnz  6156  xpdifid  6165  xpdifcnvepel  6166  ssrnres  6176  dfrel2  6187  resssxp  6271  relrelss  6274  unixp0  6284  reuop  6294  dfpo2  6297  fn0  6666  funssxp  6734  f00  6760  f0bi  6761  dffo2  6796  f1o00  6856  fo00  6857  fv3  6899  dffn5  6939  dff2  7094  dff3  7095  dffo4  7098  dffo5  7099  exfo  7100  fmpt  7105  fompt  7113  ffnfv  7114  fsn  7131  fsn2  7132  funop  7146  funsneqopb  7149  fnsnbOLD  7164  isores1  7332  ssoprab2b  7479  eqoprab2bw  7480  eqfnov2  7540  unexb  7744  uniexb  7759  pwexb  7761  iunpw  7766  ordeleqon  7777  dford5  7779  onintrab  7791  ordsuc  7806  unon  7823  onuninsuci  7832  ordzsl  7837  onzsl  7838  f1oexbi  7921  ffoss  7939  1st2ndb  8022  frxp3  8143  suppssov1  8189  suppssov2  8190  suppssfv  8194  reldmtpos  8226  dfrecs3  8355  omopthi  8643  brinxper  8720  ecopover  8815  fsetexb  8857  mapsncnv  8887  mptelixpg  8929  elixpsn  8931  ixpsnf1o  8932  bren2  8976  en0  9011  en0ALT  9012  en0r  9013  en1  9017  en1b  9018  sbthb  9082  dom0  9089  canth2  9114  onfin2  9197  sdom1  9206  1sdom2dom  9210  fineqv  9223  unfilem1  9261  unfib  9265  pwfir  9272  pwfi  9274  fiint  9282  residfi  9291  unifpw  9308  wofib  9503  sucprcreg  9564  sucprcregOLD  9565  opthreg  9583  suc11reg  9584  infeq5  9602  rankwflemb  9761  r1elss  9774  pwwf  9775  unwf  9778  uniwf  9787  rankonid  9797  rankr1id  9830  rankuni  9831  rankxplim3  9849  scott0  9856  karden  9877  djuexb  9891  isnum3  9936  oncard  9942  card1  9950  cardlim  9954  cardmin2  9981  pm54.43lem  9982  ween  10015  acnnum  10032  alephsuc2  10060  alephgeom  10062  iscard3  10073  dfac3  10101  dfac4  10102  dfac5lem3  10105  dfac5  10108  dfac2  10111  dfac8  10115  dfac9  10116  dfacacn  10121  dfac13  10122  dfac12r  10126  dfac12k  10127  kmlem2  10131  kmlem13  10142  djuinf  10168  ackbij2  10221  cflim2  10242  isfin4-2  10293  isfin4p1  10294  isf33lem  10345  compsscnv  10350  fin1a2lem6  10384  domtriom  10422  ac9  10462  ac9s  10472  fodomb  10505  brdom3  10507  brdom5  10508  brdom4  10509  brdom7disj  10510  brdom6disj  10511  iunfo  10518  sdomsdomcard  10539  gch2  10655  gch3  10656  eltsk2g  10731  grutsk  10802  ordpipq  10922  ltbtwnnq  10958  mappsrpr  11088  map2psrpr  11090  elreal2  11112  le2tri3i  11335  elnn0nn  12541  elnnnn0b  12543  elnnnn0c  12544  elnnz  12596  elnn0z  12599  elz2  12604  elnnz1  12615  eluz2b2  12940  elnn1uz2  12944  elpqb  12995  elioo4g  13428  eluzfz2b  13556  fzn0  13561  elfz1end  13578  fzass4  13586  elfz1b  13617  nn0fz0  13649  fzolb  13690  fzon0  13702  elfzo0  13725  elfzo0z  13726  elfzo1  13737  fzo1fzo0n0  13740  om2uzrani  13984  nn0opthi  14302  hashkf  14364  isfinite4  14394  hashprb  14429  hashf1  14490  elss2prb  14521  iswrdb  14553  wrdexb  14558  0wrd0  14573  wrdl3s3  14995  cotr2g  15009  trclun  15047  rexanuz  15393  rexuz3  15396  fsum0diag  15824  fprod0diag  16036  divalgmod  16459  sadcp1  16508  isprm6  16768  nnoddn2prmb  16868  4sqlem4  17007  fnpr2ob  17607  mreunirn  17648  isdrs2  18357  isacs5  18599  isacs4  18600  isacs3  18601  dfgrp2  19024  dfgrp3  19100  dfgrp3e  19101  isnsg3  19221  gicer  19342  oppgmndb  19420  oppggrpb  19423  pmtrfb  19530  invghm  19898  isringrng  20366  opprrngb  20424  opprringb  20426  ricer  20604  isnzr2hash  20617  isdomn4  20814  abvn0b  20939  gzrngunit  21583  dvdsrzring  21611  zringunit  21616  zlmlmod  21672  cygth  21721  frgpcyg  21723  zlmassa  22053  toprntopon  23082  tgclb  23127  iscldtop  23252  isnrm2  23515  isnrm3  23516  discmp  23555  dfconn2  23576  2ndcsb  23606  dis2ndc  23617  loclly  23644  unisngl  23684  locfindis  23687  iskgen2  23705  dfac14  23775  kqtop  23902  kqt0  23903  kqreg  23908  kqnrm  23909  hmpher  23941  hmphsymb  23943  hmph0  23952  kqhmph  23976  ist1-5lem  23977  elmptrab2  23985  isfil2  24013  filunirn  24039  isufil2  24065  hausflim  24138  isfcls  24166  alexsubALT  24208  istgp2  24248  ustbas  24384  xmetunirn  24494  dscmet  24729  dscopn  24730  isngp4  24769  zcld  24971  zlmclm  25271  iscmet2  25453  iundisj  25707  i1f1lem  25848  fta1b  26329  elply2  26353  elqaa  26483  aannenlem2  26492  wilth  27235  lgsne0  27499  2lgs  27571  2sqlem2  27582  ostth  27803  elno2  27818  bdayfo  27841  elons2  28451  eln0s2  28550  eln0s  28554  elzn0s  28591  eln0zs  28593  elnnzs  28594  remulscllem1  28693  mpteleeOLD  29245  wrdupgr  29435  wrdumgr  29447  umgrislfupgr  29473  uspgrupgrushgr  29529  usgrumgruspgr  29532  usgruspgrb  29533  usgrislfuspgr  29537  uvtx01vtx  29747  pthspthcyc  30152  wwlksnwwlksnon  30264  elwwlks2ons3  30304  clwwlkn1loopb  30394  eclclwwlkn1  30426  upgriseupth  30558  numclwwlkovh  30724  nmlno0lem  31145  isblo3i  31153  blocni  31157  hvsubeq0i  31415  hvaddcani  31417  bcseqi  31472  isch3  31593  norm1exi  31602  hhsssh  31621  shslubi  31737  dfch2  31759  pjoc1i  31783  pjchi  31784  shs00i  31802  chsscon3i  31813  chlejb1i  31828  chj00i  31839  shjshseli  31845  h1de2ctlem  31907  spanunsni  31931  cmcmi  31944  cmbr3i  31952  cmbr4i  31953  pj11i  32063  hosubeq0i  32178  dmadjrnb  32258  nmlnop0iALT  32347  lnopeq0i  32359  elunop2  32365  lnconi  32385  lncnopbd  32389  adjbdlnb  32436  adjbd1o  32437  adjeq0  32443  rnbra  32459  pjss1coi  32515  pjss2coi  32516  pjnormssi  32520  pjssdif2i  32526  pjssdif1i  32527  dfpjop  32534  pjinvari  32543  pjin2i  32545  pjci  32552  pjcmul1i  32553  pjcmul2i  32554  strb  32610  hstrbi  32618  mdsl1i  32673  atom1d  32705  chrelat2i  32717  cvbr4i  32719  cvexchi  32721  sumdmdi  32772  dmdbr4ati  32773  dmdbr5ati  32774  dmdbr6ati  32775  dmdbr7ati  32776  cdj3i  32793  eqtrb  32820  difeq  32864  iundisjf  32934  fpwrelmap  33078  iundisjfi  33141  xrge0tsmsbi  33394  dflring2  33783  dfufd2  33840  0mplrim  33904  ccfldextdgrr  34062  issgon  34513  measbasedom  34592  oddpwdc  34744  eulerpartlemt  34761  ballotlem2  34879  ballotlemrinv  34924  bnj1533  35240  bnj983  35339  r1omhf  35500  r1omhfb  35508  fineqvomonb  35532  fineqvnttrclse  35537  r1omhfbregs  35550  fineqvr1ombregs  35551  kardeq0  35569  karddom  35574  kardsdom  35575  kardexen  35576  0nn0m1nnn0  35604  lfuhgr3  35612  spthcycl  35621  satfv1  35855  satf0op  35869  fmla0xp  35875  fmla1  35879  elmsta  36040  antnestlaw1  36183  antnestlaw2  36184  antnestlaw3  36185  nepss  36210  dfon2  36282  distel  36293  fnimage  36419  altopthsn  36453  ellines  36644  rankeq1o  36663  opnrebl2  36832  df3nandALT1  36910  ttc00  37019  ttcwf  37035  ttcwf2  37036  ttcexbi  37044  ttc0el  37046  bj-animbi  37151  bj-dfbi6  37168  bj-consensus  37171  bj-falor2  37178  bj-bibibi  37179  bj-andnotim  37181  bj-alextruim  37259  bj-exextruan  37260  bj-ssbeq  37275  bj-19.41al  37281  bj-subst  37283  bj-eqs  37298  bj-cbvexw  37299  bj-sb  37312  bj-substax12  37349  bj-dfnnf3  37406  bj-equs45fv  37446  bj-hbaeb2  37453  bj-hbnaeb  37455  bj-equsal  37461  bj-sbsb  37472  bj-moeub  37484  bj-csbsnlem  37538  bj-snsetex  37599  bj-snglex  37609  bj-1uplth  37643  bj-1uplex  37644  bj-2uplth  37657  bj-2uplex  37658  bj-bm1.3ii  37700  bj-restpw  37734  bj-restuni  37739  bj-discrmoore  37753  bj-snmooreb  37756  bj-elid6  37814  bj-eldiag2  37821  mptsnunlem  37984  topdifinf  37995  elxp8  38017  finxp1o  38038  wl-moae  38171  wl-exeq  38189  wl-aleq  38190  wl-nfeqfb  38191  volsupnfl  38316  cover2  38366  isbnd3  38435  cntotbnd  38447  heibor  38472  isfld2  38656  isfldidl  38719  orfa  38733  eqbrb  38888  eqelb  38890  iss2  38993  issetssr  39232  n0el3  39385  detlem  39535  petlem  39564  eldisjs6  39589  prtlem16  39643  isltrn2N  40894  aks6d1c2p2  42886  aks6d1c6isolem3  42943  sn-iotalem  42992  dffltz  43366  eu6w  43408  3cubes  43421  ismrc  43432  isnacs3  43441  rexzrexnn0  43531  eldioph4b  43538  dford3  43755  wopprc  43757  ttac  43763  pw2f1ocnv  43764  dfac11  43789  dfac21  43793  isnumbasabl  43833  isnumbasgrp  43834  dfacbasgrp  43835  aaitgo  43889  dflim5  44056  nvocnvb  44148  dfno2  44154  ifpbi1b  44229  rp-fakeimass  44238  rp-fakeanorass  44239  rp-isfinite5  44243  rp-isfinite6  44244  dfsucon  44249  snen1g  44250  iscard4  44259  rtrclex  44343  cnvtrrel  44396  frege54cor0a  44589  isotone1  44774  isotone2  44775  gneispace  44860  k0004lem3  44875  grumnueq  44997  ismnushort  45011  nanorxor  45015  nzss  45027  pm10.55  45079  pm11.57  45099  pm13.192  45120  pm13.194  45122  ipo0  45158  ifr0  45159  xpexb  45162  3impexpbicom  45189  com3rgbi  45223  pm2.43bgbi  45226  pm2.43cbi  45227  sb5ALT  45234  trsbc  45249  2pm13.193  45261  ax6e2ndeq  45268  2uasbanh  45270  eelT01  45419  eel0T1  45420  uunT1  45488  zfregs2VD  45549  equncomVD  45576  trsbcVD  45585  undif3VD  45590  2pm13.193VD  45611  ax6e2eqVD  45615  ax6e2ndeqVD  45617  2uasbanhVD  45619  ax6e2ndeqALT  45639  tcfr  45672  mptssid  45956  elfzfzo  45996  allbutfi  46108  uzn0bi  46173  dvnprodlem3  46662  elaa2  46948  sge00  47090  elhoi  47256  ovn0  47280  ovolval4lem2  47364  confun  47676  afvfv0bi  47889  ffnafv  47908  afv2ndefb  47961  dfatafv2rnb  47964  afv2fv0b  48003  prpair  48250  sbcpr  48270  fpprel2  48506  sbgoldbmb  48551  vopnbgrelself  48620  isgrtri  48708  stgr1  48726  mgm2mgm  48992  nnpw2pb  49367  0aryfvalel  49414  mo0sn  49594  resinsnlem  49649  homf0  49787  isoval2  49813  oppccicb  49829  oppcciceq  49830  funcf2lem2  49860  initc  49869  isinito2  50277  isinito3  50278  termc  50297  dftermc3  50309  elsetrecs  50478  elpg  50492