Theorem impbii 208

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bicom  221  biid  260  2th  263  pm5.74  269  bitri  274  notnotb  315  con34b  316  notbi  319  bibi2i  338  con1b  359  con2b  360  bi2.04  389  imdi  391  pm4.8  393  pm4.81  394  impexp  451  ancom  461  anass  469  jcab  518  impimprbi  826  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  1046  consensus  1050  3impexp  1357  3jaob  1425  nanass  1505  norassOLD  1536  tbw-bijust  1701  tbw-negdf  1702  19.26  1873  19.35  1880  19.21v  1942  19.23v  1945  19.41v  1953  19.3v  1985  19.9v  1987  equcom  2021  cbvalw  2038  exexw  2054  sbbii  2079  sban  2083  sbv  2091  alcom  2156  19.3  2195  19.41  2228  sbalex  2235  equsexv  2260  sbim  2300  cbvalv1  2338  cbval  2398  equsex  2418  aecom  2427  equs45f  2459  dfsb1  2485  dfsb2  2497  sb6f  2501  dfmoeu  2536  moabs  2543  mobii  2548  mo3  2564  mo4  2566  exmoeu  2581  moanimlem  2620  euan  2623  euanv  2626  2mo  2650  2eu6  2658  euae  2661  axextb  2712  eqcom  2745  nebi  3024  r19.26  3095  r19.35  3269  ralcom3  3289  cgsex4g  3473  ceqsex  3475  ceqsexv  3476  gencbvex  3485  gencbvex2  3486  pm13.183  3596  rr19.3v  3597  rr19.28v  3598  euxfr2w  3654  euxfr2  3656  reu6  3660  reu3  3661  reuan  3828  sspss  4033  complss  4080  unineq  4211  uneqin  4212  difrab  4242  ab0w  4307  sbnfc2  4370  un00  4376  disj  4381  ssdifeq0  4417  r19.2zb  4426  ralidmw  4438  ralidm  4442  ralf0  4444  pwidb  4556  snidb  4596  rabsnifsb  4658  tppreqb  4738  difsnb  4739  pwpw0  4746  sssn  4759  preq12b  4781  pwsnOLD  4832  unissint  4903  uniintsn  4918  iununi  5027  al0ssb  5230  intex  5259  intnex  5260  iin0  5282  axpweq  5285  nfcvb  5297  eusvnfb  5314  eusv2nf  5316  ralxfrALT  5336  sspwb  5363  unipw  5364  opnz  5386  opth  5389  sbcop1  5400  opeqsng  5415  propeqop  5419  opthwiener  5426  opthhausdorff  5429  opthhausdorff0  5430  rexopabb  5438  ssopab2bw  5457  ssopab2b  5459  pwssun  5480  opelxp  5620  opthprc  5646  relsnb  5705  relop  5752  issetid  5756  xpid11  5834  elinxp  5922  eldmeldmressn  5928  iss  5936  iresn0n0  5956  asymref2  6015  xpnz  6055  xpdifid  6064  ssrnres  6074  dfrel2  6085  resssxp  6166  relrelss  6169  unixp0  6179  reuop  6189  dfpo2  6192  fn0  6556  funssxp  6621  f00  6648  f0bi  6649  dffo2  6684  f1o00  6743  fo00  6744  fv3  6784  dffn5  6820  dff2  6967  dff3  6968  dffo4  6971  dffo5  6972  exfo  6973  fmpt  6976  ffnfv  6984  fsn  6999  fsn2  7000  funop  7013  funsneqopb  7016  fnsnb  7030  isores1  7197  ssoprab2b  7334  eqoprab2bw  7335  eqfnov2  7394  unexb  7588  uniexb  7604  pwexb  7606  iunpw  7611  ordeleqon  7622  onintrab  7636  unon  7668  onuninsuci  7677  ordzsl  7682  onzsl  7683  f1oexbi  7765  ffoss  7778  1st2ndb  7860  suppssov1  8001  suppssfv  8005  reldmtpos  8037  dfrecs3  8190  dfrecs3OLD  8191  omopthi  8478  ecopover  8597  fsetexb  8639  mapsncnv  8668  mptelixpg  8710  elixpsn  8712  ixpsnf1o  8713  bren2  8758  en0  8790  en0OLD  8791  en0ALT  8792  en0r  8793  en1  8798  en1OLD  8799  en1b  8800  en1bOLD  8801  sbthb  8868  dom0  8876  canth2  8904  pwfir  8946  pwfi  8948  onfin2  9001  sdom1  9009  1sdom  9012  fineqv  9025  unfilem1  9065  fiint  9078  residfi  9087  pwfiOLD  9101  unifpw  9109  wofib  9291  sucprcreg  9347  opthreg  9363  suc11reg  9364  infeq5  9382  rankwflemb  9561  r1elss  9574  pwwf  9575  unwf  9578  uniwf  9587  rankonid  9597  rankr1id  9630  rankuni  9631  rankxplim3  9649  scott0  9654  karden  9663  djuexb  9677  isnum3  9722  oncard  9728  card1  9736  cardlim  9740  cardmin2  9767  pm54.43lem  9768  ween  9801  acnnum  9818  alephsuc2  9846  alephgeom  9848  iscard3  9859  dfac3  9887  dfac4  9888  dfac5lem3  9891  dfac5  9894  dfac2  9897  dfac8  9901  dfac9  9902  dfacacn  9907  dfac13  9908  dfac12r  9912  dfac12k  9913  kmlem2  9917  kmlem13  9928  djuinf  9954  ackbij2  10009  cflim2  10029  isfin4-2  10080  isfin4p1  10081  isf33lem  10132  compsscnv  10137  fin1a2lem6  10171  domtriom  10209  ac9  10249  ac9s  10259  fodomb  10292  brdom3  10294  brdom5  10295  brdom4  10296  brdom7disj  10297  brdom6disj  10298  iunfo  10305  sdomsdomcard  10326  gch2  10441  gch3  10442  eltsk2g  10517  grutsk  10588  ordpipq  10708  ltbtwnnq  10744  mappsrpr  10874  map2psrpr  10876  elreal2  10898  le2tri3i  11115  elnn0nn  12285  elnnnn0b  12287  elnnnn0c  12288  elnnz  12339  elnn0z  12342  elz2  12347  elnnz1  12356  eluz2b2  12671  elnn1uz2  12675  elpqb  12726  elioo4g  13149  eluzfz2b  13275  fzn0  13280  elfz1end  13296  fzass4  13304  elfz1b  13335  nn0fz0  13364  fzolb  13403  fzon0  13415  elfzo0  13438  elfzo0z  13439  elfzo1  13447  fzo1fzo0n0  13448  om2uzrani  13682  nn0opthi  13994  hashkf  14056  isfinite4  14087  hashprb  14122  hashf1  14181  elss2prb  14211  iswrdb  14233  wrdexb  14238  0wrd0  14253  wrdl3s3  14687  cotr2g  14697  trclun  14735  sqr0lem  14962  rexanuz  15067  rexuz3  15070  fsum0diag  15499  fprod0diag  15706  divalgmod  16125  sadcp1  16172  isprm6  16429  nnoddn2prmb  16524  4sqlem4  16663  fnpr2ob  17279  mreunirn  17320  isdrs2  18034  isacs5  18276  isacs4  18277  isacs3  18278  dfgrp2  18614  dfgrp3  18684  dfgrp3e  18685  isnsg3  18798  gicer  18902  oppgmndb  18972  oppggrpb  18975  pmtrfb  19083  invghm  19445  opprringb  19884  isnzr2hash  20545  abvn0b  20583  gzrngunit  20674  dvdsrzring  20693  zringunit  20698  zlmlmod  20738  cygth  20789  frgpcyg  20791  zlmassa  21116  toprntopon  22084  tgclb  22130  iscldtop  22256  isnrm2  22519  isnrm3  22520  discmp  22559  dfconn2  22580  2ndcsb  22610  dis2ndc  22621  loclly  22648  unisngl  22688  locfindis  22691  iskgen2  22709  dfac14  22779  kqtop  22906  kqt0  22907  kqreg  22912  kqnrm  22913  hmpher  22945  hmphsymb  22947  hmph0  22956  kqhmph  22980  ist1-5lem  22981  elmptrab2  22989  isfil2  23017  filunirn  23043  isufil2  23069  hausflim  23142  isfcls  23170  alexsubALT  23212  istgp2  23252  ustbas  23389  xmetunirn  23500  dscmet  23738  dscopn  23739  isngp4  23778  zcld  23986  zlmclm  24285  iscmet2  24468  iundisj  24722  i1f1lem  24863  fta1b  25344  elply2  25367  elqaa  25492  aannenlem2  25499  wilth  26230  lgsne0  26493  2lgs  26565  2sqlem2  26576  ostth  26797  mptelee  27273  wrdupgr  27465  wrdumgr  27477  umgrislfupgr  27503  uspgrupgrushgr  27557  usgrumgruspgr  27560  usgruspgrb  27561  usgrislfuspgr  27564  uvtx01vtx  27774  wwlksnwwlksnon  28288  elwwlks2ons3  28328  clwwlkn1loopb  28415  eclclwwlkn1  28447  upgriseupth  28579  numclwwlkovh  28745  nmlno0lem  29163  isblo3i  29171  blocni  29175  hvsubeq0i  29433  hvaddcani  29435  bcseqi  29490  isch3  29611  norm1exi  29620  hhsssh  29639  shslubi  29755  dfch2  29777  pjoc1i  29801  pjchi  29802  shs00i  29820  chsscon3i  29831  chlejb1i  29846  chj00i  29857  shjshseli  29863  h1de2ctlem  29925  spanunsni  29949  cmcmi  29962  cmbr3i  29970  cmbr4i  29971  pj11i  30081  hosubeq0i  30196  dmadjrnb  30276  nmlnop0iALT  30365  lnopeq0i  30377  elunop2  30383  lnconi  30403  lncnopbd  30407  adjbdlnb  30454  adjbd1o  30455  adjeq0  30461  rnbra  30477  pjss1coi  30533  pjss2coi  30534  pjnormssi  30538  pjssdif2i  30544  pjssdif1i  30545  dfpjop  30552  pjinvari  30561  pjin2i  30563  pjci  30570  pjcmul1i  30571  pjcmul2i  30572  strb  30628  hstrbi  30636  mdsl1i  30691  atom1d  30723  chrelat2i  30735  cvbr4i  30737  cvexchi  30739  sumdmdi  30790  dmdbr4ati  30791  dmdbr5ati  30792  dmdbr6ati  30793  dmdbr7ati  30794  cdj3i  30811  eqtrb  30831  difeq  30873  iundisjf  30936  cnvoprabOLD  31063  fpwrelmap  31076  iundisjfi  31125  xrge0tsmsbi  31326  ccfldextdgrr  31750  issgon  32099  measbasedom  32178  oddpwdc  32329  eulerpartlemt  32346  ballotlem2  32463  ballotlemrinv  32508  bnj1533  32840  bnj983  32939  0nn0m1nnn0  33079  lfuhgr3  33089  spthcycl  33099  satfv1  33333  satf0op  33347  fmla0xp  33353  fmla1  33357  elmsta  33518  nepss  33670  dford5  33679  dfon2  33776  distel  33787  frxp3  33805  elno2  33865  bdayfo  33888  fnimage  34239  altopthsn  34271  ellines  34462  rankeq1o  34481  opnrebl2  34518  df3nandALT1  34596  bj-animbi  34747  bj-dfbi6  34764  bj-consensus  34767  bj-falor2  34775  bj-bibibi  34776  bj-andnotim  34778  bj-cbval  34838  bj-cbvex  34839  bj-ssbeq  34842  bj-19.41al  34848  bj-subst  34850  bj-eqs  34864  bj-cbvexw  34865  bj-sb  34877  bj-substax12  34911  bj-dfnnf3  34947  bj-equs45fv  35001  bj-hbaeb2  35009  bj-hbnaeb  35011  bj-equsal  35017  bj-sbsb  35028  bj-moeub  35041  bj-csbsnlem  35096  bj-snsetex  35161  bj-snglex  35171  bj-1uplth  35205  bj-1uplex  35206  bj-2uplth  35219  bj-2uplex  35220  bj-bm1.3ii  35243  bj-restpw  35271  bj-restuni  35276  bj-discrmoore  35290  bj-snmooreb  35293  bj-elid6  35349  bj-eldiag2  35356  mptsnunlem  35517  topdifinf  35528  elxp8  35550  finxp1o  35571  wl-moae  35683  wl-exeq  35701  wl-aleq  35702  wl-nfeqfb  35703  wl-ax11-lem6  35749  volsupnfl  35830  cover2  35880  isbnd3  35950  cntotbnd  35962  heibor  35987  isfld2  36171  isfldidl  36234  orfa  36248  eqelb  36390  iss2  36487  issetssr  36629  n0el3  36771  prtlem16  36891  isltrn2N  38142  isdomn4  40180  sn-iotalem  40197  dffltz  40479  3cubes  40520  ismrc  40531  isnacs3  40540  rexzrexnn0  40634  eldioph4b  40641  dford3  40858  wopprc  40860  ttac  40866  pw2f1ocnv  40867  dfac11  40895  dfac21  40899  isnumbasabl  40939  isnumbasgrp  40940  dfacbasgrp  40941  aaitgo  40995  ifpbi1b  41100  rp-fakeimass  41109  rp-fakeanorass  41110  rp-isfinite5  41114  rp-isfinite6  41115  dfsucon  41120  snen1g  41121  iscard4  41130  rtrclex  41206  cnvtrrel  41259  frege54cor0a  41452  isotone1  41639  isotone2  41640  gneispace  41725  k0004lem3  41740  grumnueq  41886  ismnushort  41900  nanorxor  41904  nzss  41916  pm10.55  41968  pm11.57  41988  pm13.192  42009  pm13.194  42011  ipo0  42048  ifr0  42049  xpexb  42053  3impexpbicom  42080  com3rgbi  42115  pm2.43bgbi  42118  pm2.43cbi  42119  sb5ALT  42126  trsbc  42141  2pm13.193  42153  ax6e2ndeq  42160  2uasbanh  42162  eelT01  42312  eel0T1  42313  uunT1  42381  zfregs2VD  42442  equncomVD  42469  trsbcVD  42478  undif3VD  42483  2pm13.193VD  42504  ax6e2eqVD  42508  ax6e2ndeqVD  42510  2uasbanhVD  42512  ax6e2ndeqALT  42532  fompt  42711  mptssid  42766  elfzfzo  42796  allbutfi  42914  uzn0bi  42980  dvnprodlem3  43470  elaa2  43756  sge00  43895  elhoi  44061  ovn0  44085  ovolval4lem2  44169  confun  44412  afvfv0bi  44622  ffnafv  44641  afv2ndefb  44694  dfatafv2rnb  44697  afv2fv0b  44736  prpair  44931  sbcpr  44951  fpprel2  45171  sbgoldbmb  45216  mgm2mgm  45399  isringrng  45417  nnpw2pb  45911  0aryfvalel  45958  mo0sn  46139  elsetrecs  46383  elpg  46397