Theorem impbii 199

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  dfbi1  203  bicom  212  biid  251  2th  254  pm5.74  259  bitri  264  notnotb  304  con34b  305  notbi  308  bibi2i  326  con1b  347  con2b  348  bi2.04  375  pm5.4  376  imdi  377  pm4.8  379  pm4.81  380  impexp  437  ancom  452  anass  459  jcab  503  pm4.45im  818  orcom  851  dfor2  879  oridm  882  orbi2i  890  or12  898  biorfi  916  pm4.72  926  oibabs  928  jaob  936  pm4.44  972  pm4.79  977  andi  981  annotanannotOLD  985  pm4.82  1005  cases2ALT  1033  consensus  1039  3impexp  1451  3jaob  1538  tbw-bijust  1771  tbw-negdf  1772  19.26  1949  19.35  1957  19.21v  2020  19.23v  2023  19.41v  2029  sbbii  2056  19.9v  2065  19.23vOLD  2071  19.41vOLD  2082  equcom  2103  equvinvOLD  2116  equvelvOLD  2119  cbvalw  2124  alcom  2193  19.3  2224  19.41  2259  sb6  2272  cbvalv1  2336  19.3OLD  2364  cbval  2432  cbvalv  2434  equsex  2447  aecom  2463  equs45f  2496  dfsb2  2520  sb6f  2532  sbim  2542  sb6OLD  2576  mo2v  2625  exmoeu  2651  mo3  2656  moanim  2678  euan  2679  2mo  2700  2eu6  2707  axext4  2755  eqcom  2778  nebi  3023  r19.26  3212  ralcom3  3253  ceqsex  3393  gencbvex  3402  gencbvex2  3403  clel5  3495  pm13.183  3496  rr19.3v  3497  rr19.28v  3498  euxfr2  3544  reu6  3548  reu3  3549  sspss  3857  complss  3903  unineq  4027  uneqin  4028  difrab  4050  sbnfc2  4152  un00  4156  ssdifeq0  4194  r19.2zb  4203  snidb  4347  rabsnifsb  4394  ssdifsnOLD  4456  tppreqb  4472  difsnb  4473  pwpw0  4480  sssn  4493  preq12b  4514  pwsnALT  4568  unissint  4636  uniintsn  4649  iununi  4745  intex  4952  intnex  4953  iin0  4971  axpweq  4974  eusvnfb  4994  eusv2nf  4996  ralxfrALT  5016  nfcvb  5027  sspwb  5046  unipw  5047  opnz  5070  opth  5073  opeqsng  5095  propeqop  5101  opthwiener  5108  opthhausdorff  5111  opthhausdorff0  5112  ssopab2b  5136  pwssun  5154  opelxp  5287  opthprc  5308  relop  5412  issetid  5416  xpid11  5486  elres  5577  eldmeldmressn  5582  iss  5589  restidsingOLD  5601  issref  5651  asymref2  5655  xpnz  5695  xpdifid  5704  ssrnres  5714  dfrel2  5725  relrelss  5804  unixp0  5814  fn0  6152  funssxp  6202  f00  6228  f0bi  6229  dffo2  6261  f1o00  6313  fo00  6314  fv3  6348  dffn5  6384  dff2  6515  dff3  6516  dffo4  6519  dffo5  6520  exfo  6521  fmpt  6524  ffnfv  6531  fsn  6546  fsn2  6547  funop  6558  funsneqopb  6563  fnsnb  6577  isores1  6728  ssoprab2b  6860  eqfnov2  6915  unexb  7106  uniexb  7121  pwexb  7123  iunpw  7126  ordeleqon  7136  onintrab  7149  unon  7179  onuninsuci  7188  ordzsl  7193  onzsl  7194  f1oexbi  7264  ffoss  7275  1st2ndb  7356  suppssov1  7480  suppssfv  7484  reldmtpos  7513  dfrecs3  7623  omopthi  7892  ecopover  8005  mapsncnv  8059  mptelixpg  8100  elixpsn  8102  ixpsnf1o  8103  bren2  8141  en0  8173  en1  8177  en1b  8178  sbthb  8238  canth2  8270  onfin2  8309  sdom1  8317  1sdom  8320  fineqv  8332  unfilem1  8381  fiint  8394  residfi  8404  pwfi  8418  unifpw  8426  wofib  8607  sucprcreg  8663  opthreg  8678  opthregOLD  8680  suc11reg  8681  infeq5  8699  rankwflemb  8821  r1elss  8834  pwwf  8835  unwf  8838  uniwf  8847  rankonid  8857  rankr1id  8890  rankuni  8891  rankxplim3  8909  scott0  8914  karden  8923  isnum3  8981  oncard  8987  card1  8995  cardlim  8999  cardmin2  9025  pm54.43lem  9026  ween  9059  acnnum  9076  alephsuc2  9104  alephgeom  9106  iscard3  9117  dfac3  9145  dfac4  9146  dfac5lem3  9149  dfac5  9152  dfac2  9155  dfac2OLD  9156  dfac8  9160  dfac9  9161  dfacacn  9166  dfac13  9167  dfac12r  9171  dfac12k  9172  kmlem2  9176  kmlem13  9187  cdainf  9217  ackbij2  9268  cflim2  9288  isfin4-2  9339  isfin4-3  9340  isf33lem  9391  compsscnv  9396  fin1a2lem6  9430  domtriom  9468  ac9  9508  ac9s  9518  fodomb  9551  brdom3  9553  brdom5  9554  brdom4  9555  brdom7disj  9556  brdom6disj  9557  iunfo  9564  sdomsdomcard  9585  gch2  9700  gch3  9701  eltsk2g  9776  grutsk  9847  grothpw  9851  ordpipq  9967  ltbtwnnq  10003  mappsrpr  10132  map2psrpr  10134  elreal2  10156  le2tri3i  10370  elnn0nn  11538  elnnnn0b  11540  elnnnn0c  11541  elnnz  11590  elnn0z  11593  elz2  11597  elnnz1  11606  eluz2b2  11965  elnn1uz2  11969  elioo4g  12440  eluzfz2b  12558  fzn0  12563  elfz1end  12579  fzass4  12587  elfz1b  12617  nn0fz0  12646  fzolb  12685  fzon0  12696  elfzo0  12718  elfzo0z  12719  elfzo1  12727  fzo1fzo0n0  12728  om2uzrani  12960  nn0opthi  13262  hashkf  13324  isfinite4  13356  hashprb  13388  hashf1  13444  elss2prb  13472  iswrdb  13508  wrdexb  13513  0wrd0  13528  wrdl3s3  13916  cotr2g  13926  trclun  13964  sqr0lem  14190  rexanuz  14294  rexuz3  14297  fsum0diag  14717  fprod0diag  14924  divalgmod  15338  sadcp1  15386  isprm6  15634  nnoddn2prmb  15726  4sqlem4  15864  mreunirn  16470  isdrs2  17148  isacs5  17381  isacs4  17382  isacs3  17383  dfgrp2  17656  dfgrp3  17723  dfgrp3e  17724  isnsg3  17837  gicer  17927  oppgmndb  17993  oppggrpb  17996  pmtrfb  18093  invghm  18447  opprringb  18841  isnzr2hash  19480  abvn0b  19518  gzrngunit  20028  dvdsrzring  20047  zringunit  20052  zlmlmod  20087  zlmassa  20088  cygth  20136  frgpcyg  20138  toprntopon  20951  tgclb  20996  iscldtop  21121  isnrm2  21384  isnrm3  21385  discmp  21423  dfconn2  21444  2ndcsb  21474  dis2ndc  21485  loclly  21512  unisngl  21552  locfindis  21555  iskgen2  21573  dfac14  21643  kqtop  21770  kqt0  21771  kqreg  21776  kqnrm  21777  hmpher  21809  hmphsymb  21811  hmph0  21820  kqhmph  21844  ist1-5lem  21845  elmptrab2  21853  isfil2  21881  filunirn  21907  isufil2  21933  hausflim  22006  isfcls  22034  alexsubALT  22076  istgp2  22116  ustbas  22252  xmetunirn  22363  dscmet  22598  dscopn  22599  isngp4  22637  zcld  22837  zlmclm  23132  iscmet2  23312  iundisj  23537  i1f1lem  23677  fta1b  24150  elply2  24173  elqaa  24298  aannenlem2  24305  wilth  25019  lgsne0  25282  2lgs  25354  2sqlem2  25365  ostth  25550  mptelee  25997  wrdupgr  26202  wrdumgr  26214  umgrislfupgr  26240  uspgrupgrushgr  26295  usgrumgruspgr  26298  usgruspgrb  26299  usgrislfuspgr  26302  uvtx01vtx  26526  uvtxa01vtx0OLD  26528  wwlksnwwlksnon  27061  elwwlks2ons3  27103  clwwlknclwwlkdifsOLD  27130  clwwlkn1loopb  27200  eclclwwlkn1  27234  upgriseupth  27388  numclwwlkovh  27565  nmlno0lem  27989  isblo3i  27997  blocni  28001  hvsubeq0i  28261  hvaddcani  28263  bcseqi  28318  isch3  28439  norm1exi  28448  hhsssh  28467  shslubi  28585  dfch2  28607  pjoc1i  28631  pjchi  28632  shs00i  28650  chsscon3i  28661  chlejb1i  28676  chj00i  28687  shjshseli  28693  h1de2ctlem  28755  spanunsni  28779  cmcmi  28792  cmbr3i  28800  cmbr4i  28801  pj11i  28911  hosubeq0i  29026  dmadjrnb  29106  nmlnop0iALT  29195  lnopeq0i  29207  elunop2  29213  lnconi  29233  lncnopbd  29237  adjbdlnb  29284  adjbd1o  29285  adjeq0  29291  rnbra  29307  pjss1coi  29363  pjss2coi  29364  pjnormssi  29368  pjssdif2i  29374  pjssdif1i  29375  dfpjop  29382  pjinvari  29391  pjin2i  29393  pjci  29400  pjcmul1i  29401  pjcmul2i  29402  strb  29458  hstrbi  29466  mdsl1i  29521  atom1d  29553  chrelat2i  29565  cvbr4i  29567  cvexchi  29569  sumdmdi  29620  dmdbr4ati  29621  dmdbr5ati  29622  dmdbr6ati  29623  dmdbr7ati  29624  cdj3i  29641  difeq  29694  iundisjf  29741  cnvoprabOLD  29839  fpwrelmap  29849  iundisjfi  29896  xrge0tsmsbi  30127  issgon  30527  measbasedom  30606  oddpwdc  30757  eulerpartlemt  30774  ballotlem2  30891  ballotlemrinv  30936  bnj1533  31261  bnj983  31360  elmsta  31784  nepss  31938  dford5  31947  dfpo2  31984  dfon2  32034  distel  32046  elno2  32145  bdayfo  32166  fnimage  32374  altopthsn  32406  ellines  32597  rankeq1o  32616  opnrebl2  32654  df3nandALT1  32734  pm4.81ALT  32884  bj-dfbi6  32898  bj-consensus  32900  bj-falor2  32908  bj-bibibi  32909  bj-andnotim  32911  bj-ssbeq  32966  bj-ssb0  32967  bj-19.41al  32975  bj-sb56  32977  bj-eqs  33001  bj-cbvexw  33002  bj-sb  33015  bj-equs45fv  33089  bj-sbfvv  33102  bj-sb6  33104  bj-axext4  33107  bj-hbaeb2  33141  bj-hbnaeb  33143  bj-equsal  33149  bj-sbsb  33160  bj-mo3OLD  33168  bj-cleqhyp  33222  bj-csbsnlem  33228  bj-snsetex  33283  bj-snglex  33293  bj-1uplth  33327  bj-1uplex  33328  bj-2uplth  33341  bj-2uplex  33342  bj-bm1.3ii  33356  bj-restpw  33378  bj-restuni  33383  bj-ismooredr2  33398  bj-discrmoore  33399  bj-snmoore  33401  bj-elid  33423  bj-elid3  33425  bj-eldiag2  33430  mptsnunlem  33523  topdifinf  33535  elxp8  33557  finxp1o  33567  wl-nfnbi  33650  wl-exeq  33657  wl-aleq  33658  wl-nfeqfb  33659  wl-ax11-lem6  33702  volsupnfl  33788  cover2  33841  isbnd3  33916  cntotbnd  33928  heibor  33953  isfld2  34137  isfldidl  34200  orfa  34214  eqelb  34348  iss2  34455  issetssr  34596  prtlem16  34678  isltrn2N  35929  elpwbi  37779  ismrc  37791  isnacs3  37800  rexzrexnn0  37895  eldioph4b  37902  dford3  38122  wopprc  38124  ttac  38130  pw2f1ocnv  38131  dfac11  38159  dfac21  38163  isnumbasabl  38203  isnumbasgrp  38204  dfacbasgrp  38205  aaitgo  38259  ifpbi1b  38375  rp-fakeimass  38384  rp-fakeanorass  38385  rp-fakenanass  38387  rp-isfinite5  38390  rp-isfinite6  38391  rtrclex  38451  cnvtrrel  38489  rp-imass  38592  frege54cor0a  38684  isotone1  38873  isotone2  38874  gneispace  38959  k0004lem3  38974  nanorxor  39031  nzss  39043  pm10.55  39095  pm11.57  39116  sbeqalbi  39128  pm13.192  39138  pm13.194  39140  ipo0  39179  ifr0  39180  xpexb  39184  3impexpbicom  39211  com3rgbi  39246  pm2.43bgbi  39249  pm2.43cbi  39250  sb5ALT  39257  trsbc  39276  2pm13.193  39294  ax6e2ndeq  39301  2uasbanh  39303  eelT01  39462  eel0T1  39463  uunT1  39533  zfregs2VD  39599  equncomVD  39627  trsbcVD  39636  undif3VD  39641  2pm13.193VD  39662  ax6e2eqVD  39666  ax6e2ndeqVD  39668  2uasbanhVD  39670  ax6e2ndeqALT  39690  fompt  39900  mptssid  39969  elfzfzo  40007  allbutfi  40133  uzn0bi  40206  dvnprodlem3  40682  elaa2  40969  sge00  41111  ismea  41186  elhoi  41277  ovn0  41301  ovolval4lem2  41385  confun  41627  reuan  41701  afvfv0bi  41753  ffnafv  41772  sbgoldbmb  42203  mgm2mgm  42392  isringrng  42410  nnpw2pb  42910  elsetrecs  42975  elpg  42989