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  1019  andi  1023  pm4.82  1039  cases2ALT  1062  consensus  1066  3impexp  1375  nanass  1537  tbw-bijust  1725  tbw-negdf  1726  19.26  1897  19.35  1904  19.21v  1966  19.23v  1969  19.41v  1976  19.3v  2009  19.9v  2011  equcom  2045  cbvalw  2062  alcomw  2072  excomw  2073  exexw  2080  dfsb  2100  sbbii  2116  sban  2120  sbv  2128  sbrimvw  2131  alcom  2200  19.3  2244  19.41  2277  sbalex  2284  sbalexOLD  2285  equsexv  2310  sbim  2344  cbvalv1  2379  cbval  2436  equsex  2456  aecom  2465  equs45f  2497  dfsb1  2519  dfsb2  2531  sb6f  2535  dfmoeu  2569  moabs  2577  mo3  2598  mo4  2600  exmoeu  2615  moanimlem  2652  euan  2655  euanv  2658  2mo  2682  2eu6  2690  euae  2693  axextb  2744  eqcom  2776  nebi  3044  r19.35  3129  r19.26  3131  r19.21v  3196  gencbvex  3519  gencbvex2  3520  pm13.183  3634  rr19.3v  3635  rr19.28v  3636  euxfr2w  3692  euxfr2  3694  reu6  3698  reu3  3699  reuan  3858  dfss2  3931  sspss  4064  complss  4113  unineq  4249  uneqin  4250  difrab  4279  sbnfc2  4402  un00  4408  ssdifeq0  4449  r19.2zb  4463  ralidmw  4479  ralidm  4480  pwidb  4586  snidb  4629  rabsnifsb  4690  tppreqb  4774  difsnb  4775  pwpw0  4780  sssn  4793  preq12b  4816  unissint  4938  uniintsn  4951  iununi  5066  al0ssb  5270  intex  5312  intnex  5313  axpweq  5319  iin0  5331  nfcvb  5345  eusvnfb  5362  eusv2nf  5364  ralxfrALT  5384  sspwb  5428  unipw  5429  opnz  5453  opth  5456  sbcop1  5468  opeqsng  5484  propeqop  5488  opthwiener  5495  opthhausdorff  5498  opthhausdorff0  5499  rexopabb  5510  ssopab2bw  5530  ssopab2b  5532  pwssun  5551  opelxp  5695  opthprc  5723  relsnb  5787  relop  5834  issetid  5838  xpid11  5920  elinxp  6016  eldmeldmressn  6022  iss  6035  iresn0n0  6054  asymref2  6115  xpnz  6154  xpdifid  6163  xpdifcnvepel  6164  ssrnres  6174  dfrel2  6185  resssxp  6269  relrelss  6272  unixp0  6282  reuop  6292  dfpo2  6295  fn0  6664  funssxp  6732  f00  6758  f0bi  6759  dffo2  6794  f1o00  6854  fo00  6855  fv3  6897  dffn5  6937  dff2  7092  dff3  7093  dffo4  7096  dffo5  7097  exfo  7098  fmpt  7103  fompt  7111  ffnfv  7112  fsn  7129  fsn2  7130  funop  7144  funsneqopb  7147  fnsnbOLD  7162  isores1  7330  ssoprab2b  7477  eqoprab2bw  7478  eqfnov2  7538  unexb  7742  unexbOLD  7743  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  10243  isfin4-2  10294  isfin4p1  10295  isf33lem  10346  compsscnv  10351  fin1a2lem6  10385  domtriom  10423  ac9  10463  ac9s  10473  fodomb  10506  brdom3  10508  brdom5  10509  brdom4  10510  brdom7disj  10511  brdom6disj  10512  iunfo  10519  sdomsdomcard  10540  gch2  10656  gch3  10657  eltsk2g  10732  grutsk  10803  ordpipq  10923  ltbtwnnq  10959  mappsrpr  11089  map2psrpr  11091  elreal2  11113  le2tri3i  11336  elnn0nn  12542  elnnnn0b  12544  elnnnn0c  12545  elnnz  12597  elnn0z  12600  elz2  12605  elnnz1  12616  eluz2b2  12941  elnn1uz2  12945  elpqb  12996  elioo4g  13429  eluzfz2b  13557  fzn0  13562  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  16460  sadcp1  16509  isprm6  16769  nnoddn2prmb  16869  4sqlem4  17008  fnpr2ob  17608  mreunirn  17649  isdrs2  18358  isacs5  18600  isacs4  18601  isacs3  18602  dfgrp2  19025  dfgrp3  19101  dfgrp3e  19102  isnsg3  19222  gicer  19343  oppgmndb  19421  oppggrpb  19424  pmtrfb  19531  invghm  19899  isringrng  20366  opprrngb  20424  opprringb  20426  isnzr2hash  20599  isdomn4  20796  abvn0b  20913  gzrngunit  21548  dvdsrzring  21576  zringunit  21581  zlmlmod  21637  cygth  21686  frgpcyg  21688  zlmassa  22018  toprntopon  23047  tgclb  23092  iscldtop  23217  isnrm2  23480  isnrm3  23481  discmp  23520  dfconn2  23541  2ndcsb  23571  dis2ndc  23582  loclly  23609  unisngl  23649  locfindis  23652  iskgen2  23670  dfac14  23740  kqtop  23867  kqt0  23868  kqreg  23873  kqnrm  23874  hmpher  23906  hmphsymb  23908  hmph0  23917  kqhmph  23941  ist1-5lem  23942  elmptrab2  23950  isfil2  23978  filunirn  24004  isufil2  24030  hausflim  24103  isfcls  24131  alexsubALT  24173  istgp2  24213  ustbas  24349  xmetunirn  24459  dscmet  24694  dscopn  24695  isngp4  24734  zcld  24936  zlmclm  25236  iscmet2  25418  iundisj  25672  i1f1lem  25813  fta1b  26294  elply2  26318  elqaa  26448  aannenlem2  26455  wilth  27197  lgsne0  27461  2lgs  27533  2sqlem2  27544  ostth  27765  elno2  27780  bdayfo  27803  elons2  28413  eln0s2  28512  eln0s  28516  elzn0s  28553  eln0zs  28555  elnnzs  28556  remulscllem1  28655  mpteleeOLD  29182  wrdupgr  29372  wrdumgr  29384  umgrislfupgr  29410  uspgrupgrushgr  29466  usgrumgruspgr  29469  usgruspgrb  29470  usgrislfuspgr  29474  uvtx01vtx  29684  pthspthcyc  30089  wwlksnwwlksnon  30201  elwwlks2ons3  30241  clwwlkn1loopb  30331  eclclwwlkn1  30363  upgriseupth  30495  numclwwlkovh  30661  nmlno0lem  31082  isblo3i  31090  blocni  31094  hvsubeq0i  31352  hvaddcani  31354  bcseqi  31409  isch3  31530  norm1exi  31539  hhsssh  31558  shslubi  31674  dfch2  31696  pjoc1i  31720  pjchi  31721  shs00i  31739  chsscon3i  31750  chlejb1i  31765  chj00i  31776  shjshseli  31782  h1de2ctlem  31844  spanunsni  31868  cmcmi  31881  cmbr3i  31889  cmbr4i  31890  pj11i  32000  hosubeq0i  32115  dmadjrnb  32195  nmlnop0iALT  32284  lnopeq0i  32296  elunop2  32302  lnconi  32322  lncnopbd  32326  adjbdlnb  32373  adjbd1o  32374  adjeq0  32380  rnbra  32396  pjss1coi  32452  pjss2coi  32453  pjnormssi  32457  pjssdif2i  32463  pjssdif1i  32464  dfpjop  32471  pjinvari  32480  pjin2i  32482  pjci  32489  pjcmul1i  32490  pjcmul2i  32491  strb  32547  hstrbi  32555  mdsl1i  32610  atom1d  32642  chrelat2i  32654  cvbr4i  32656  cvexchi  32658  sumdmdi  32709  dmdbr4ati  32710  dmdbr5ati  32711  dmdbr6ati  32712  dmdbr7ati  32713  cdj3i  32730  eqtrb  32757  difeq  32801  iundisjf  32871  fpwrelmap  33015  iundisjfi  33078  xrge0tsmsbi  33331  dflring2  33724  dfufd2  33781  0mplrim  33845  ccfldextdgrr  34003  issgon  34454  measbasedom  34533  oddpwdc  34685  eulerpartlemt  34702  ballotlem2  34820  ballotlemrinv  34865  bnj1533  35181  bnj983  35280  r1omhf  35438  r1omhfb  35444  fineqvomonb  35451  fineqvnttrclse  35456  r1omhfbregs  35469  fineqvr1ombregs  35470  0nn0m1nnn0  35499  lfuhgr3  35507  spthcycl  35516  satfv1  35750  satf0op  35764  fmla0xp  35770  fmla1  35774  elmsta  35935  antnestlaw1  36078  antnestlaw2  36079  antnestlaw3  36080  nepss  36105  dfon2  36177  distel  36188  fnimage  36314  altopthsn  36348  ellines  36539  rankeq1o  36558  opnrebl2  36717  df3nandALT1  36795  ttc00  36904  ttcwf  36920  ttcwf2  36921  ttcexbi  36929  ttc0el  36931  bj-animbi  37036  bj-dfbi6  37053  bj-consensus  37056  bj-falor2  37063  bj-bibibi  37064  bj-andnotim  37066  bj-alextruim  37144  bj-exextruan  37145  bj-ssbeq  37160  bj-19.41al  37166  bj-subst  37168  bj-eqs  37183  bj-cbvexw  37184  bj-sb  37197  bj-substax12  37234  bj-dfnnf3  37291  bj-equs45fv  37331  bj-hbaeb2  37338  bj-hbnaeb  37340  bj-equsal  37346  bj-sbsb  37357  bj-moeub  37369  bj-csbsnlem  37423  bj-snsetex  37483  bj-snglex  37493  bj-1uplth  37527  bj-1uplex  37528  bj-2uplth  37541  bj-2uplex  37542  bj-bm1.3ii  37584  bj-restpw  37617  bj-restuni  37622  bj-discrmoore  37636  bj-snmooreb  37639  bj-elid6  37697  bj-eldiag2  37704  mptsnunlem  37867  topdifinf  37878  elxp8  37900  finxp1o  37921  wl-moae  38054  wl-exeq  38072  wl-aleq  38073  wl-nfeqfb  38074  volsupnfl  38199  cover2  38249  isbnd3  38318  cntotbnd  38330  heibor  38355  isfld2  38539  isfldidl  38602  orfa  38616  eqbrb  38773  eqelb  38775  iss2  38878  issetssr  39117  n0el3  39270  detlem  39420  petlem  39449  eldisjs6  39474  prtlem16  39528  isltrn2N  40779  aks6d1c2p2  42771  aks6d1c6isolem3  42828  sn-iotalem  42877  dffltz  43253  eu6w  43295  3cubes  43308  ismrc  43319  isnacs3  43328  rexzrexnn0  43418  eldioph4b  43425  dford3  43642  wopprc  43644  ttac  43650  pw2f1ocnv  43651  dfac11  43676  dfac21  43680  isnumbasabl  43720  isnumbasgrp  43721  dfacbasgrp  43722  aaitgo  43776  dflim5  43943  nvocnvb  44035  dfno2  44041  ifpbi1b  44116  rp-fakeimass  44125  rp-fakeanorass  44126  rp-isfinite5  44130  rp-isfinite6  44131  dfsucon  44136  snen1g  44137  iscard4  44146  rtrclex  44230  cnvtrrel  44283  frege54cor0a  44476  isotone1  44661  isotone2  44662  gneispace  44747  k0004lem3  44762  grumnueq  44884  ismnushort  44898  nanorxor  44902  nzss  44914  pm10.55  44966  pm11.57  44986  pm13.192  45007  pm13.194  45009  ipo0  45045  ifr0  45046  xpexb  45049  3impexpbicom  45076  com3rgbi  45110  pm2.43bgbi  45113  pm2.43cbi  45114  sb5ALT  45121  trsbc  45136  2pm13.193  45148  ax6e2ndeq  45155  2uasbanh  45157  eelT01  45306  eel0T1  45307  uunT1  45375  zfregs2VD  45436  equncomVD  45463  trsbcVD  45472  undif3VD  45477  2pm13.193VD  45498  ax6e2eqVD  45502  ax6e2ndeqVD  45504  2uasbanhVD  45506  ax6e2ndeqALT  45526  tcfr  45559  mptssid  45843  elfzfzo  45883  allbutfi  45995  uzn0bi  46060  dvnprodlem3  46549  elaa2  46835  sge00  46977  elhoi  47143  ovn0  47167  ovolval4lem2  47251  confun  47560  afvfv0bi  47773  ffnafv  47792  afv2ndefb  47845  dfatafv2rnb  47848  afv2fv0b  47887  prpair  48134  sbcpr  48154  fpprel2  48390  sbgoldbmb  48435  vopnbgrelself  48504  isgrtri  48592  stgr1  48610  mgm2mgm  48876  nnpw2pb  49247  0aryfvalel  49294  mo0sn  49474  resinsnlem  49529  homf0  49667  isoval2  49693  oppccicb  49709  oppcciceq  49710  funcf2lem2  49740  initc  49749  isinito2  50157  isinito3  50158  termc  50177  dftermc3  50189  elsetrecs  50358  elpg  50372