Theorem impbii 209

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bicom  222  biid  261  2th  264  pm5.74  270  bitri  275  notnotb  315  con34b  316  notbi  319  bibi2i  337  con1b  358  con2b  359  bi2.04  387  imdi  389  pm4.8  392  pm4.81  393  impexp  450  ancom  460  anass  468  jcab  517  impimprbi  828  orcom  870  dfor2  901  oridm  904  orbi2i  912  or12  920  biorfriOLD  940  pm4.72  951  oibabs  953  jaob  963  pm4.44  998  pm4.79  1005  andi  1009  pm4.82  1025  cases2ALT  1048  consensus  1052  3impexp  1359  3jaobOLD  1429  nanass  1510  tbw-bijust  1698  tbw-negdf  1699  19.26  1870  19.35  1877  19.21v  1939  19.23v  1942  19.41v  1949  19.3v  1982  19.9v  1984  equcom  2018  cbvalw  2035  alcomw  2045  exexw  2052  sbbii  2077  sban  2081  sbv  2089  alcom  2160  19.3  2203  19.41  2236  sbalex  2243  sbalexOLD  2244  equsexv  2269  sbim  2303  cbvalv1  2339  cbval  2397  equsex  2417  aecom  2426  equs45f  2458  dfsb1  2480  dfsb2  2492  sb6f  2496  dfmoeu  2530  moabs  2537  mobii  2542  mo3  2558  mo4  2560  exmoeu  2575  moanimlem  2612  euan  2615  euanv  2618  2mo  2642  2eu6  2651  euae  2654  axextb  2705  eqcom  2737  nebi  3006  ralcom3OLD  3081  r19.35  3089  r19.35OLD  3090  r19.26  3092  r19.21v  3159  ceqsexOLD  3500  gencbvex  3510  gencbvex2  3511  pm13.183  3635  rr19.3v  3636  rr19.28v  3637  euxfr2w  3694  euxfr2  3696  reu6  3700  reu3  3701  reuan  3862  dfss2  3935  sspss  4068  complss  4117  unineq  4254  uneqin  4255  difrab  4284  ab0w  4345  sbnfc2  4405  un00  4411  disj  4416  ssdifeq0  4453  r19.2zb  4462  ralidmw  4474  ralidm  4478  ralf0  4480  pwidb  4587  snidb  4628  rabsnifsb  4689  tppreqb  4772  difsnb  4773  pwpw0  4780  sssn  4793  preq12b  4817  unissint  4939  uniintsn  4952  iununi  5066  al0ssb  5266  intex  5302  intnex  5303  axpweq  5309  iin0  5320  nfcvb  5334  eusvnfb  5351  eusv2nf  5353  ralxfrALT  5373  sspwb  5412  unipw  5413  opnz  5436  opth  5439  sbcop1  5451  opeqsng  5466  propeqop  5470  opthwiener  5477  opthhausdorff  5480  opthhausdorff0  5481  rexopabb  5491  ssopab2bw  5510  ssopab2b  5512  pwssun  5533  opelxp  5677  opthprc  5705  relsnb  5768  relop  5817  issetid  5821  xpid11  5899  elinxp  5993  eldmeldmressn  5999  iss  6009  iresn0n0  6028  asymref2  6093  xpnz  6135  xpdifid  6144  ssrnres  6154  dfrel2  6165  resssxp  6246  relrelss  6249  unixp0  6259  reuop  6269  dfpo2  6272  fn0  6652  funssxp  6719  f00  6745  f0bi  6746  dffo2  6779  f1o00  6838  fo00  6839  fv3  6879  dffn5  6922  dff2  7074  dff3  7075  dffo4  7078  dffo5  7079  exfo  7080  fmpt  7085  fompt  7093  ffnfv  7094  fsn  7110  fsn2  7111  funop  7124  funsneqopb  7127  fnsnbOLD  7143  isores1  7312  ssoprab2b  7461  eqoprab2bw  7462  eqfnov2  7522  unexb  7726  unexbOLD  7727  uniexb  7743  pwexb  7745  iunpw  7750  ordeleqon  7761  dford5  7763  onintrab  7775  ordsuc  7791  unon  7809  onuninsuci  7819  ordzsl  7824  onzsl  7825  f1oexbi  7907  ffoss  7927  1st2ndb  8011  frxp3  8133  suppssov1  8179  suppssov2  8180  suppssfv  8184  reldmtpos  8216  dfrecs3  8344  omopthi  8628  brinxper  8703  ecopover  8797  fsetexb  8840  mapsncnv  8869  mptelixpg  8911  elixpsn  8913  ixpsnf1o  8914  bren2  8957  en0  8992  en0ALT  8993  en0r  8994  en1  8998  en1b  8999  sbthb  9068  dom0  9075  canth2  9100  onfin2  9186  sdom1  9196  sdom1OLD  9197  1sdom2dom  9201  1sdomOLD  9203  fineqv  9217  unfilem1  9261  unfib  9265  pwfir  9273  pwfi  9275  fiint  9284  fiintOLD  9285  residfi  9296  unifpw  9313  wofib  9505  sucprcreg  9561  opthreg  9578  suc11reg  9579  infeq5  9597  rankwflemb  9753  r1elss  9766  pwwf  9767  unwf  9770  uniwf  9779  rankonid  9789  rankr1id  9822  rankuni  9823  rankxplim3  9841  scott0  9846  karden  9855  djuexb  9869  isnum3  9914  oncard  9920  card1  9928  cardlim  9932  cardmin2  9959  pm54.43lem  9960  ween  9995  acnnum  10012  alephsuc2  10040  alephgeom  10042  iscard3  10053  dfac3  10081  dfac4  10082  dfac5lem3  10085  dfac5  10089  dfac2  10092  dfac8  10096  dfac9  10097  dfacacn  10102  dfac13  10103  dfac12r  10107  dfac12k  10108  kmlem2  10112  kmlem13  10123  djuinf  10149  ackbij2  10202  cflim2  10223  isfin4-2  10274  isfin4p1  10275  isf33lem  10326  compsscnv  10331  fin1a2lem6  10365  domtriom  10403  ac9  10443  ac9s  10453  fodomb  10486  brdom3  10488  brdom5  10489  brdom4  10490  brdom7disj  10491  brdom6disj  10492  iunfo  10499  sdomsdomcard  10520  gch2  10635  gch3  10636  eltsk2g  10711  grutsk  10782  ordpipq  10902  ltbtwnnq  10938  mappsrpr  11068  map2psrpr  11070  elreal2  11092  le2tri3i  11311  elnn0nn  12491  elnnnn0b  12493  elnnnn0c  12494  elnnz  12546  elnn0z  12549  elz2  12554  elnnz1  12566  eluz2b2  12887  elnn1uz2  12891  elpqb  12942  elioo4g  13374  eluzfz2b  13501  fzn0  13506  elfz1end  13522  fzass4  13530  elfz1b  13561  nn0fz0  13593  fzolb  13633  fzon0  13645  elfzo0  13668  elfzo0z  13669  elfzo1  13680  fzo1fzo0n0  13683  om2uzrani  13924  nn0opthi  14242  hashkf  14304  isfinite4  14334  hashprb  14369  hashf1  14429  elss2prb  14460  iswrdb  14492  wrdexb  14497  0wrd0  14512  wrdl3s3  14935  cotr2g  14949  trclun  14987  rexanuz  15319  rexuz3  15322  fsum0diag  15750  fprod0diag  15959  divalgmod  16383  sadcp1  16432  isprm6  16691  nnoddn2prmb  16791  4sqlem4  16930  fnpr2ob  17528  mreunirn  17569  isdrs2  18274  isacs5  18514  isacs4  18515  isacs3  18516  dfgrp2  18901  dfgrp3  18978  dfgrp3e  18979  isnsg3  19099  gicer  19216  oppgmndb  19294  oppggrpb  19297  pmtrfb  19402  invghm  19770  isringrng  20203  opprrngb  20262  opprringb  20264  isnzr2hash  20435  isdomn4  20632  abvn0b  20752  gzrngunit  21357  dvdsrzring  21378  zringunit  21383  zlmlmod  21439  cygth  21488  frgpcyg  21490  zlmassa  21819  toprntopon  22819  tgclb  22864  iscldtop  22989  isnrm2  23252  isnrm3  23253  discmp  23292  dfconn2  23313  2ndcsb  23343  dis2ndc  23354  loclly  23381  unisngl  23421  locfindis  23424  iskgen2  23442  dfac14  23512  kqtop  23639  kqt0  23640  kqreg  23645  kqnrm  23646  hmpher  23678  hmphsymb  23680  hmph0  23689  kqhmph  23713  ist1-5lem  23714  elmptrab2  23722  isfil2  23750  filunirn  23776  isufil2  23802  hausflim  23875  isfcls  23903  alexsubALT  23945  istgp2  23985  ustbas  24122  xmetunirn  24232  dscmet  24467  dscopn  24468  isngp4  24507  zcld  24709  zlmclm  25019  iscmet2  25201  iundisj  25456  i1f1lem  25597  fta1b  26084  elply2  26108  elqaa  26237  aannenlem2  26244  wilth  26988  lgsne0  27253  2lgs  27325  2sqlem2  27336  ostth  27557  elno2  27573  bdayfo  27596  elons2  28166  eln0s  28258  elzn0s  28293  eln0zs  28295  elnnzs  28296  remulscllem1  28358  mptelee  28829  wrdupgr  29019  wrdumgr  29031  umgrislfupgr  29057  uspgrupgrushgr  29113  usgrumgruspgr  29116  usgruspgrb  29117  usgrislfuspgr  29121  uvtx01vtx  29331  pthspthcyc  29740  wwlksnwwlksnon  29852  elwwlks2ons3  29892  clwwlkn1loopb  29979  eclclwwlkn1  30011  upgriseupth  30143  numclwwlkovh  30309  nmlno0lem  30729  isblo3i  30737  blocni  30741  hvsubeq0i  30999  hvaddcani  31001  bcseqi  31056  isch3  31177  norm1exi  31186  hhsssh  31205  shslubi  31321  dfch2  31343  pjoc1i  31367  pjchi  31368  shs00i  31386  chsscon3i  31397  chlejb1i  31412  chj00i  31423  shjshseli  31429  h1de2ctlem  31491  spanunsni  31515  cmcmi  31528  cmbr3i  31536  cmbr4i  31537  pj11i  31647  hosubeq0i  31762  dmadjrnb  31842  nmlnop0iALT  31931  lnopeq0i  31943  elunop2  31949  lnconi  31969  lncnopbd  31973  adjbdlnb  32020  adjbd1o  32021  adjeq0  32027  rnbra  32043  pjss1coi  32099  pjss2coi  32100  pjnormssi  32104  pjssdif2i  32110  pjssdif1i  32111  dfpjop  32118  pjinvari  32127  pjin2i  32129  pjci  32136  pjcmul1i  32137  pjcmul2i  32138  strb  32194  hstrbi  32202  mdsl1i  32257  atom1d  32289  chrelat2i  32301  cvbr4i  32303  cvexchi  32305  sumdmdi  32356  dmdbr4ati  32357  dmdbr5ati  32358  dmdbr6ati  32359  dmdbr7ati  32360  cdj3i  32377  eqtrb  32410  difeq  32454  iundisjf  32525  fpwrelmap  32663  iundisjfi  32726  xrge0tsmsbi  33010  dfufd2  33528  ccfldextdgrr  33674  issgon  34120  measbasedom  34199  oddpwdc  34352  eulerpartlemt  34369  ballotlem2  34487  ballotlemrinv  34532  bnj1533  34849  bnj983  34948  0nn0m1nnn0  35107  lfuhgr3  35114  spthcycl  35123  satfv1  35357  satf0op  35371  fmla0xp  35377  fmla1  35381  elmsta  35542  antnestlaw1  35685  antnestlaw2  35686  antnestlaw3  35687  nepss  35712  dfon2  35787  distel  35798  fnimage  35924  altopthsn  35956  ellines  36147  rankeq1o  36166  opnrebl2  36316  df3nandALT1  36394  bj-animbi  36554  bj-dfbi6  36570  bj-consensus  36573  bj-falor2  36580  bj-bibibi  36581  bj-andnotim  36583  bj-cbval  36644  bj-cbvex  36645  bj-ssbeq  36648  bj-19.41al  36654  bj-subst  36656  bj-eqs  36670  bj-cbvexw  36671  bj-sb  36682  bj-substax12  36716  bj-dfnnf3  36752  bj-equs45fv  36806  bj-hbaeb2  36813  bj-hbnaeb  36815  bj-equsal  36821  bj-sbsb  36832  bj-moeub  36844  bj-csbsnlem  36898  bj-snsetex  36958  bj-snglex  36968  bj-1uplth  37002  bj-1uplex  37003  bj-2uplth  37016  bj-2uplex  37017  bj-bm1.3ii  37059  bj-restpw  37087  bj-restuni  37092  bj-discrmoore  37106  bj-snmooreb  37109  bj-elid6  37165  bj-eldiag2  37172  mptsnunlem  37333  topdifinf  37344  elxp8  37366  finxp1o  37387  wl-moae  37511  wl-exeq  37529  wl-aleq  37530  wl-nfeqfb  37531  wl-ax11-lem6  37585  volsupnfl  37666  cover2  37716  isbnd3  37785  cntotbnd  37797  heibor  37822  isfld2  38006  isfldidl  38069  orfa  38083  eqbrb  38228  eqelb  38230  iss2  38333  issetssr  38501  n0el3  38650  detlem  38782  petlem  38811  prtlem16  38869  isltrn2N  40121  aks6d1c2p2  42114  aks6d1c6isolem3  42171  sn-iotalem  42216  dffltz  42629  eu6w  42671  3cubes  42685  ismrc  42696  isnacs3  42705  rexzrexnn0  42799  eldioph4b  42806  dford3  43024  wopprc  43026  ttac  43032  pw2f1ocnv  43033  dfac11  43058  dfac21  43062  isnumbasabl  43102  isnumbasgrp  43103  dfacbasgrp  43104  aaitgo  43158  dflim5  43325  nvocnvb  43418  dfno2  43424  ifpbi1b  43499  rp-fakeimass  43508  rp-fakeanorass  43509  rp-isfinite5  43513  rp-isfinite6  43514  dfsucon  43519  snen1g  43520  iscard4  43529  rtrclex  43613  cnvtrrel  43666  frege54cor0a  43859  isotone1  44044  isotone2  44045  gneispace  44130  k0004lem3  44145  grumnueq  44283  ismnushort  44297  nanorxor  44301  nzss  44313  pm10.55  44365  pm11.57  44385  pm13.192  44406  pm13.194  44408  ipo0  44445  ifr0  44446  xpexb  44450  3impexpbicom  44477  com3rgbi  44511  pm2.43bgbi  44514  pm2.43cbi  44515  sb5ALT  44522  trsbc  44537  2pm13.193  44549  ax6e2ndeq  44556  2uasbanh  44558  eelT01  44707  eel0T1  44708  uunT1  44776  zfregs2VD  44837  equncomVD  44864  trsbcVD  44873  undif3VD  44878  2pm13.193VD  44899  ax6e2eqVD  44903  ax6e2ndeqVD  44905  2uasbanhVD  44907  ax6e2ndeqALT  44927  tcfr  44960  mptssid  45242  elfzfzo  45282  allbutfi  45396  uzn0bi  45462  dvnprodlem3  45953  elaa2  46239  sge00  46381  elhoi  46547  ovn0  46571  ovolval4lem2  46655  confun  46944  afvfv0bi  47157  ffnafv  47176  afv2ndefb  47229  dfatafv2rnb  47232  afv2fv0b  47271  prpair  47506  sbcpr  47526  fpprel2  47746  sbgoldbmb  47791  vopnbgrelself  47859  isgrtri  47946  stgr1  47964  mgm2mgm  48219  nnpw2pb  48580  0aryfvalel  48627  mo0sn  48808  resinsnlem  48863  homf0  49002  isoval2  49028  oppccicb  49044  oppcciceq  49045  funcf2lem2  49075  initc  49084  isinito2  49492  isinito3  49493  termc  49512  dftermc3  49524  elsetrecs  49693  elpg  49707