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  341  con1b  362  con2b  363  bi2.04  392  imdi  394  pm4.8  396  pm4.81  397  impexp  454  ancom  464  anass  472  jcab  521  impimprbi  827  orcom  867  dfor2  899  oridm  902  orbi2i  910  or12  918  biorfi  936  pm4.72  947  oibabs  949  jaob  959  pm4.44  994  pm4.79  1001  andi  1005  pm4.82  1021  cases2ALT  1044  consensus  1048  3impexp  1355  3jaob  1423  nanass  1501  norassOLD  1535  tbw-bijust  1700  tbw-negdf  1701  19.26  1871  19.35  1878  19.21v  1940  19.23v  1943  19.41v  1950  19.3v  1986  19.9v  1988  equcom  2025  cbvalw  2042  sbbii  2081  sban  2085  sbv  2095  alcom  2160  19.3  2200  19.41  2235  sbbibOLD  2285  sbim  2307  sbimvOLD  2318  cbvalv1  2350  cbval  2405  cbvalvOLD  2409  equsex  2429  aecom  2438  equs45f  2471  dfsb1  2499  dfsb2  2511  sb6f  2515  sbbiiALT  2554  sb6ALT  2561  dfsb2ALT  2567  sb6fALT  2578  sbimALT  2584  dfmoeu  2594  moabs  2601  mobii  2606  mo3  2623  mo4  2625  exmoeu  2641  moanimlem  2680  euan  2683  euanv  2686  2mo  2710  2eu6  2719  euae  2722  axextb  2773  eqcom  2805  nebi  3067  r19.26  3137  r19.35  3295  ralcom3  3317  cgsex4g  3486  ceqsex  3488  gencbvex  3497  gencbvex2  3498  pm13.183  3606  rr19.3v  3607  rr19.28v  3608  euxfr2w  3659  euxfr2  3661  reu6  3665  reu3  3666  reuan  3825  sspss  4027  complss  4074  unineq  4204  uneqin  4205  difrab  4229  sbnfc2  4344  un00  4350  disj  4355  ssdifeq0  4390  r19.2zb  4399  pwidb  4520  snidb  4560  rabsnifsb  4618  tppreqb  4698  difsnb  4699  pwpw0  4706  sssn  4719  preq12b  4741  pwsnOLD  4793  unissint  4862  uniintsn  4875  iununi  4984  al0ssb  5176  intex  5204  intnex  5205  iin0  5226  axpweq  5230  nfcvb  5242  eusvnfb  5259  eusv2nf  5261  ralxfrALT  5281  sspwb  5307  unipw  5308  opnz  5330  opth  5333  sbcop1  5344  opeqsng  5358  propeqop  5362  opthwiener  5369  opthhausdorff  5372  opthhausdorff0  5373  rexopabb  5380  ssopab2bw  5399  ssopab2b  5401  pwssun  5421  opelxp  5555  opthprc  5580  relsnb  5639  relop  5685  issetid  5689  xpid11  5766  elinxp  5856  eldmeldmressn  5862  iss  5870  iresn0n0  5890  asymref2  5944  xpnz  5983  xpdifid  5992  ssrnres  6002  dfrel2  6013  resssxp  6089  relrelss  6092  unixp0  6102  reuop  6112  fn0  6451  funssxp  6509  f00  6535  f0bi  6536  dffo2  6569  f1o00  6624  fo00  6625  fv3  6663  dffn5  6699  dff2  6842  dff3  6843  dffo4  6846  dffo5  6847  exfo  6848  fmpt  6851  ffnfv  6859  fsn  6874  fsn2  6875  funop  6888  funsneqopb  6891  fnsnb  6905  isores1  7066  ssoprab2b  7202  eqoprab2bw  7203  eqfnov2  7260  unexb  7451  uniexb  7466  pwexb  7468  iunpw  7473  ordeleqon  7483  onintrab  7496  unon  7526  onuninsuci  7535  ordzsl  7540  onzsl  7541  f1oexbi  7615  ffoss  7629  1st2ndb  7711  suppssov1  7845  suppssfv  7849  reldmtpos  7883  dfrecs3  7992  omopthi  8267  ecopover  8384  mapsncnv  8440  mptelixpg  8482  elixpsn  8484  ixpsnf1o  8485  bren2  8523  en0  8555  en1  8559  en1b  8560  sbthb  8622  canth2  8654  onfin2  8695  sdom1  8702  1sdom  8705  fineqv  8717  unfilem1  8766  fiint  8779  residfi  8789  pwfi  8803  unifpw  8811  wofib  8993  sucprcreg  9049  opthreg  9065  suc11reg  9066  infeq5  9084  rankwflemb  9206  r1elss  9219  pwwf  9220  unwf  9223  uniwf  9232  rankonid  9242  rankr1id  9275  rankuni  9276  rankxplim3  9294  scott0  9299  karden  9308  djuexb  9322  isnum3  9367  oncard  9373  card1  9381  cardlim  9385  cardmin2  9412  pm54.43lem  9413  ween  9446  acnnum  9463  alephsuc2  9491  alephgeom  9493  iscard3  9504  dfac3  9532  dfac4  9533  dfac5lem3  9536  dfac5  9539  dfac2  9542  dfac8  9546  dfac9  9547  dfacacn  9552  dfac13  9553  dfac12r  9557  dfac12k  9558  kmlem2  9562  kmlem13  9573  djuinf  9599  ackbij2  9654  cflim2  9674  isfin4-2  9725  isfin4p1  9726  isf33lem  9777  compsscnv  9782  fin1a2lem6  9816  domtriom  9854  ac9  9894  ac9s  9904  fodomb  9937  brdom3  9939  brdom5  9940  brdom4  9941  brdom7disj  9942  brdom6disj  9943  iunfo  9950  sdomsdomcard  9971  gch2  10086  gch3  10087  eltsk2g  10162  grutsk  10233  ordpipq  10353  ltbtwnnq  10389  mappsrpr  10519  map2psrpr  10521  elreal2  10543  le2tri3i  10759  elnn0nn  11927  elnnnn0b  11929  elnnnn0c  11930  elnnz  11979  elnn0z  11982  elz2  11987  elnnz1  11996  eluz2b2  12309  elnn1uz2  12313  elpqb  12363  elioo4g  12785  eluzfz2b  12911  fzn0  12916  elfz1end  12932  fzass4  12940  elfz1b  12971  nn0fz0  13000  fzolb  13039  fzon0  13050  elfzo0  13073  elfzo0z  13074  elfzo1  13082  fzo1fzo0n0  13083  om2uzrani  13315  nn0opthi  13626  hashkf  13688  isfinite4  13719  hashprb  13754  hashf1  13811  elss2prb  13841  iswrdb  13863  wrdexb  13868  0wrd0  13883  wrdl3s3  14317  cotr2g  14327  trclun  14365  sqr0lem  14592  rexanuz  14697  rexuz3  14700  fsum0diag  15124  fprod0diag  15332  divalgmod  15747  sadcp1  15794  isprm6  16048  nnoddn2prmb  16140  4sqlem4  16278  fnpr2ob  16823  mreunirn  16864  isdrs2  17541  isacs5  17774  isacs4  17775  isacs3  17776  dfgrp2  18120  dfgrp3  18190  dfgrp3e  18191  isnsg3  18304  gicer  18408  oppgmndb  18475  oppggrpb  18478  pmtrfb  18585  invghm  18947  opprringb  19378  isnzr2hash  20030  abvn0b  20068  gzrngunit  20157  dvdsrzring  20176  zringunit  20181  zlmlmod  20216  cygth  20263  frgpcyg  20265  zlmassa  20588  toprntopon  21530  tgclb  21575  iscldtop  21700  isnrm2  21963  isnrm3  21964  discmp  22003  dfconn2  22024  2ndcsb  22054  dis2ndc  22065  loclly  22092  unisngl  22132  locfindis  22135  iskgen2  22153  dfac14  22223  kqtop  22350  kqt0  22351  kqreg  22356  kqnrm  22357  hmpher  22389  hmphsymb  22391  hmph0  22400  kqhmph  22424  ist1-5lem  22425  elmptrab2  22433  isfil2  22461  filunirn  22487  isufil2  22513  hausflim  22586  isfcls  22614  alexsubALT  22656  istgp2  22696  ustbas  22833  xmetunirn  22944  dscmet  23179  dscopn  23180  isngp4  23218  zcld  23418  zlmclm  23717  iscmet2  23898  iundisj  24152  i1f1lem  24293  fta1b  24770  elply2  24793  elqaa  24918  aannenlem2  24925  wilth  25656  lgsne0  25919  2lgs  25991  2sqlem2  26002  ostth  26223  mptelee  26689  wrdupgr  26878  wrdumgr  26890  umgrislfupgr  26916  uspgrupgrushgr  26970  usgrumgruspgr  26973  usgruspgrb  26974  usgrislfuspgr  26977  uvtx01vtx  27187  wwlksnwwlksnon  27701  elwwlks2ons3  27741  clwwlkn1loopb  27828  eclclwwlkn1  27860  upgriseupth  27992  numclwwlkovh  28158  nmlno0lem  28576  isblo3i  28584  blocni  28588  hvsubeq0i  28846  hvaddcani  28848  bcseqi  28903  isch3  29024  norm1exi  29033  hhsssh  29052  shslubi  29168  dfch2  29190  pjoc1i  29214  pjchi  29215  shs00i  29233  chsscon3i  29244  chlejb1i  29259  chj00i  29270  shjshseli  29276  h1de2ctlem  29338  spanunsni  29362  cmcmi  29375  cmbr3i  29383  cmbr4i  29384  pj11i  29494  hosubeq0i  29609  dmadjrnb  29689  nmlnop0iALT  29778  lnopeq0i  29790  elunop2  29796  lnconi  29816  lncnopbd  29820  adjbdlnb  29867  adjbd1o  29868  adjeq0  29874  rnbra  29890  pjss1coi  29946  pjss2coi  29947  pjnormssi  29951  pjssdif2i  29957  pjssdif1i  29958  dfpjop  29965  pjinvari  29974  pjin2i  29976  pjci  29983  pjcmul1i  29984  pjcmul2i  29985  strb  30041  hstrbi  30049  mdsl1i  30104  atom1d  30136  chrelat2i  30148  cvbr4i  30150  cvexchi  30152  sumdmdi  30203  dmdbr4ati  30204  dmdbr5ati  30205  dmdbr6ati  30206  dmdbr7ati  30207  cdj3i  30224  eqtrb  30245  difeq  30289  iundisjf  30352  cnvoprabOLD  30482  fpwrelmap  30495  iundisjfi  30545  xrge0tsmsbi  30743  ccfldextdgrr  31145  issgon  31492  measbasedom  31571  oddpwdc  31722  eulerpartlemt  31739  ballotlem2  31856  ballotlemrinv  31901  bnj1533  32234  bnj983  32333  0nn0m1nnn0  32461  lfuhgr3  32479  spthcycl  32489  satfv1  32723  satf0op  32737  fmla0xp  32743  fmla1  32747  elmsta  32908  nepss  33061  dford5  33070  dfpo2  33104  dfon2  33150  distel  33161  elno2  33274  bdayfo  33295  fnimage  33503  altopthsn  33535  ellines  33726  rankeq1o  33745  opnrebl2  33782  df3nandALT1  33860  bj-animbi  34007  bj-dfbi6  34021  bj-consensus  34024  bj-falor2  34032  bj-bibibi  34033  bj-andnotim  34035  bj-cbval  34095  bj-cbvex  34096  bj-ssbeq  34099  bj-19.41al  34105  bj-sb56  34107  bj-eqs  34121  bj-cbvexw  34122  bj-sb  34134  bj-subst  34168  bj-dfnnf3  34201  bj-equs45fv  34248  bj-hbaeb2  34256  bj-hbnaeb  34258  bj-equsal  34264  bj-sbsb  34275  bj-moeub  34288  bj-csbsnlem  34344  bj-snsetex  34399  bj-snglex  34409  bj-1uplth  34443  bj-1uplex  34444  bj-2uplth  34457  bj-2uplex  34458  bj-bm1.3ii  34481  bj-restpw  34507  bj-restuni  34512  bj-discrmoore  34526  bj-snmooreb  34529  bj-elid6  34585  bj-eldiag2  34592  mptsnunlem  34755  topdifinf  34766  elxp8  34788  finxp1o  34809  wl-moae  34921  wl-exeq  34939  wl-aleq  34940  wl-nfeqfb  34941  wl-ax11-lem6  34987  volsupnfl  35102  cover2  35152  isbnd3  35222  cntotbnd  35234  heibor  35259  isfld2  35443  isfldidl  35506  orfa  35520  eqelb  35662  iss2  35761  issetssr  35903  n0el3  36045  prtlem16  36165  isltrn2N  37416  dffltz  39615  3cubes  39631  ismrc  39642  isnacs3  39651  rexzrexnn0  39745  eldioph4b  39752  dford3  39969  wopprc  39971  ttac  39977  pw2f1ocnv  39978  dfac11  40006  dfac21  40010  isnumbasabl  40050  isnumbasgrp  40051  dfacbasgrp  40052  aaitgo  40106  ifpbi1b  40211  rp-fakeimass  40220  rp-fakeanorass  40221  rp-isfinite5  40225  rp-isfinite6  40226  dfsucon  40231  snen1g  40232  iscard4  40241  rtrclex  40317  cnvtrrel  40371  frege54cor0a  40564  isotone1  40751  isotone2  40752  gneispace  40837  k0004lem3  40852  grumnueq  40995  nanorxor  41009  nzss  41021  pm10.55  41073  pm11.57  41093  pm13.192  41114  pm13.194  41116  ipo0  41153  ifr0  41154  xpexb  41158  3impexpbicom  41185  com3rgbi  41220  pm2.43bgbi  41223  pm2.43cbi  41224  sb5ALT  41231  trsbc  41246  2pm13.193  41258  ax6e2ndeq  41265  2uasbanh  41267  eelT01  41417  eel0T1  41418  uunT1  41486  zfregs2VD  41547  equncomVD  41574  trsbcVD  41583  undif3VD  41588  2pm13.193VD  41609  ax6e2eqVD  41613  ax6e2ndeqVD  41615  2uasbanhVD  41617  ax6e2ndeqALT  41637  fompt  41819  mptssid  41877  elfzfzo  41907  allbutfi  42029  uzn0bi  42098  dvnprodlem3  42590  elaa2  42876  sge00  43015  elhoi  43181  ovn0  43205  ovolval4lem2  43289  confun  43532  afvfv0bi  43708  ffnafv  43727  afv2ndefb  43780  dfatafv2rnb  43783  afv2fv0b  43822  prpair  44018  sbcpr  44038  fpprel2  44259  sbgoldbmb  44304  mgm2mgm  44487  isringrng  44505  nnpw2pb  45001  0aryfvalel  45048  elsetrecs  45229  elpg  45243