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  829  orcom  871  dfor2  902  oridm  905  orbi2i  913  or12  921  biorfriOLD  941  pm4.72  952  oibabs  954  jaob  964  pm4.44  999  pm4.79  1006  andi  1010  pm4.82  1026  cases2ALT  1049  consensus  1053  3impexp  1360  3jaobOLD  1430  nanass  1512  tbw-bijust  1700  tbw-negdf  1701  19.26  1872  19.35  1879  19.21v  1941  19.23v  1944  19.41v  1951  19.3v  1984  19.9v  1986  equcom  2020  cbvalw  2037  alcomw  2047  excomw  2048  exexw  2055  sbbii  2082  sban  2086  sbv  2094  alcom  2165  19.3  2210  19.41  2243  sbalex  2250  sbalexOLD  2251  equsexv  2276  sbim  2310  cbvalv1  2345  cbval  2402  equsex  2422  aecom  2431  equs45f  2463  dfsb1  2485  dfsb2  2497  sb6f  2501  dfmoeu  2535  moabs  2543  mo3  2564  mo4  2566  exmoeu  2581  moanimlem  2618  euan  2621  euanv  2624  2mo  2648  2eu6  2657  euae  2660  axextb  2711  eqcom  2743  nebi  3012  r19.35  3095  r19.26  3097  r19.21v  3162  gencbvex  3487  gencbvex2  3488  pm13.183  3608  rr19.3v  3609  rr19.28v  3610  euxfr2w  3666  euxfr2  3668  reu6  3672  reu3  3673  reuan  3834  dfss2  3907  sspss  4042  complss  4091  unineq  4228  uneqin  4229  difrab  4258  sbnfc2  4379  un00  4385  ssdifeq0  4426  r19.2zb  4440  ralidmw  4456  ralidm  4457  pwidb  4562  snidb  4605  rabsnifsb  4666  tppreqb  4750  difsnb  4751  pwpw0  4756  sssn  4769  preq12b  4793  unissint  4914  uniintsn  4927  iununi  5041  al0ssb  5243  intex  5285  intnex  5286  axpweq  5292  iin0  5304  nfcvb  5318  eusvnfb  5335  eusv2nf  5337  ralxfrALT  5357  sspwb  5401  unipw  5402  opnz  5426  opth  5429  sbcop1  5441  opeqsng  5457  propeqop  5461  opthwiener  5468  opthhausdorff  5471  opthhausdorff0  5472  rexopabb  5483  ssopab2bw  5502  ssopab2b  5504  pwssun  5523  opelxp  5667  opthprc  5695  relsnb  5758  relop  5805  issetid  5809  xpid11  5887  elinxp  5984  eldmeldmressn  5990  iss  6000  iresn0n0  6019  asymref2  6080  xpnz  6123  xpdifid  6132  ssrnres  6142  dfrel2  6153  resssxp  6234  relrelss  6237  unixp0  6247  reuop  6257  dfpo2  6260  fn0  6629  funssxp  6696  f00  6722  f0bi  6723  dffo2  6756  f1o00  6815  fo00  6816  fv3  6858  dffn5  6898  dff2  7051  dff3  7052  dffo4  7055  dffo5  7056  exfo  7057  fmpt  7062  fompt  7070  ffnfv  7071  fsn  7088  fsn2  7089  funop  7103  funsneqopb  7106  fnsnbOLD  7121  isores1  7289  ssoprab2b  7436  eqoprab2bw  7437  eqfnov2  7497  unexb  7701  unexbOLD  7702  uniexb  7718  pwexb  7720  iunpw  7725  ordeleqon  7736  dford5  7738  onintrab  7750  ordsuc  7765  unon  7782  onuninsuci  7791  ordzsl  7796  onzsl  7797  f1oexbi  7879  ffoss  7899  1st2ndb  7982  frxp3  8101  suppssov1  8147  suppssov2  8148  suppssfv  8152  reldmtpos  8184  dfrecs3  8312  omopthi  8597  brinxper  8673  ecopover  8768  fsetexb  8811  mapsncnv  8841  mptelixpg  8883  elixpsn  8885  ixpsnf1o  8886  bren2  8930  en0  8965  en0ALT  8966  en0r  8967  en1  8971  en1b  8972  sbthb  9036  dom0  9043  canth2  9068  onfin2  9151  sdom1  9160  1sdom2dom  9164  fineqv  9177  unfilem1  9215  unfib  9219  pwfir  9227  pwfi  9229  fiint  9237  residfi  9248  unifpw  9265  wofib  9460  sucprcreg  9520  sucprcregOLD  9521  opthreg  9539  suc11reg  9540  infeq5  9558  rankwflemb  9717  r1elss  9730  pwwf  9731  unwf  9734  uniwf  9743  rankonid  9753  rankr1id  9786  rankuni  9787  rankxplim3  9805  scott0  9810  karden  9819  djuexb  9833  isnum3  9878  oncard  9884  card1  9892  cardlim  9896  cardmin2  9923  pm54.43lem  9924  ween  9957  acnnum  9974  alephsuc2  10002  alephgeom  10004  iscard3  10015  dfac3  10043  dfac4  10044  dfac5lem3  10047  dfac5  10051  dfac2  10054  dfac8  10058  dfac9  10059  dfacacn  10064  dfac13  10065  dfac12r  10069  dfac12k  10070  kmlem2  10074  kmlem13  10085  djuinf  10111  ackbij2  10164  cflim2  10185  isfin4-2  10236  isfin4p1  10237  isf33lem  10288  compsscnv  10293  fin1a2lem6  10327  domtriom  10365  ac9  10405  ac9s  10415  fodomb  10448  brdom3  10450  brdom5  10451  brdom4  10452  brdom7disj  10453  brdom6disj  10454  iunfo  10461  sdomsdomcard  10482  gch2  10598  gch3  10599  eltsk2g  10674  grutsk  10745  ordpipq  10865  ltbtwnnq  10901  mappsrpr  11031  map2psrpr  11033  elreal2  11055  le2tri3i  11276  elnn0nn  12479  elnnnn0b  12481  elnnnn0c  12482  elnnz  12534  elnn0z  12537  elz2  12542  elnnz1  12553  eluz2b2  12871  elnn1uz2  12875  elpqb  12926  elioo4g  13359  eluzfz2b  13487  fzn0  13492  elfz1end  13508  fzass4  13516  elfz1b  13547  nn0fz0  13579  fzolb  13620  fzon0  13632  elfzo0  13655  elfzo0z  13656  elfzo1  13667  fzo1fzo0n0  13670  om2uzrani  13914  nn0opthi  14232  hashkf  14294  isfinite4  14324  hashprb  14359  hashf1  14419  elss2prb  14450  iswrdb  14482  wrdexb  14487  0wrd0  14502  wrdl3s3  14924  cotr2g  14938  trclun  14976  rexanuz  15308  rexuz3  15311  fsum0diag  15739  fprod0diag  15951  divalgmod  16375  sadcp1  16424  isprm6  16684  nnoddn2prmb  16784  4sqlem4  16923  fnpr2ob  17522  mreunirn  17563  isdrs2  18272  isacs5  18514  isacs4  18515  isacs3  18516  dfgrp2  18938  dfgrp3  19015  dfgrp3e  19016  isnsg3  19135  gicer  19252  oppgmndb  19330  oppggrpb  19333  pmtrfb  19440  invghm  19808  isringrng  20268  opprrngb  20326  opprringb  20328  isnzr2hash  20496  isdomn4  20693  abvn0b  20813  gzrngunit  21413  dvdsrzring  21441  zringunit  21446  zlmlmod  21502  cygth  21551  frgpcyg  21553  zlmassa  21883  toprntopon  22890  tgclb  22935  iscldtop  23060  isnrm2  23323  isnrm3  23324  discmp  23363  dfconn2  23384  2ndcsb  23414  dis2ndc  23425  loclly  23452  unisngl  23492  locfindis  23495  iskgen2  23513  dfac14  23583  kqtop  23710  kqt0  23711  kqreg  23716  kqnrm  23717  hmpher  23749  hmphsymb  23751  hmph0  23760  kqhmph  23784  ist1-5lem  23785  elmptrab2  23793  isfil2  23821  filunirn  23847  isufil2  23873  hausflim  23946  isfcls  23974  alexsubALT  24016  istgp2  24056  ustbas  24192  xmetunirn  24302  dscmet  24537  dscopn  24538  isngp4  24577  zcld  24779  zlmclm  25079  iscmet2  25261  iundisj  25515  i1f1lem  25656  fta1b  26137  elply2  26161  elqaa  26288  aannenlem2  26295  wilth  27034  lgsne0  27298  2lgs  27370  2sqlem2  27381  ostth  27602  elno2  27618  bdayfo  27641  elons2  28250  eln0s2  28349  eln0s  28353  elzn0s  28390  eln0zs  28392  elnnzs  28393  remulscllem1  28492  mpteleeOLD  28964  wrdupgr  29154  wrdumgr  29166  umgrislfupgr  29192  uspgrupgrushgr  29248  usgrumgruspgr  29251  usgruspgrb  29252  usgrislfuspgr  29256  uvtx01vtx  29466  pthspthcyc  29871  wwlksnwwlksnon  29983  elwwlks2ons3  30023  clwwlkn1loopb  30113  eclclwwlkn1  30145  upgriseupth  30277  numclwwlkovh  30443  nmlno0lem  30864  isblo3i  30872  blocni  30876  hvsubeq0i  31134  hvaddcani  31136  bcseqi  31191  isch3  31312  norm1exi  31321  hhsssh  31340  shslubi  31456  dfch2  31478  pjoc1i  31502  pjchi  31503  shs00i  31521  chsscon3i  31532  chlejb1i  31547  chj00i  31558  shjshseli  31564  h1de2ctlem  31626  spanunsni  31650  cmcmi  31663  cmbr3i  31671  cmbr4i  31672  pj11i  31782  hosubeq0i  31897  dmadjrnb  31977  nmlnop0iALT  32066  lnopeq0i  32078  elunop2  32084  lnconi  32104  lncnopbd  32108  adjbdlnb  32155  adjbd1o  32156  adjeq0  32162  rnbra  32178  pjss1coi  32234  pjss2coi  32235  pjnormssi  32239  pjssdif2i  32245  pjssdif1i  32246  dfpjop  32253  pjinvari  32262  pjin2i  32264  pjci  32271  pjcmul1i  32272  pjcmul2i  32273  strb  32329  hstrbi  32337  mdsl1i  32392  atom1d  32424  chrelat2i  32436  cvbr4i  32438  cvexchi  32440  sumdmdi  32491  dmdbr4ati  32492  dmdbr5ati  32493  dmdbr6ati  32494  dmdbr7ati  32495  cdj3i  32512  eqtrb  32543  difeq  32588  iundisjf  32659  fpwrelmap  32806  iundisjfi  32869  xrge0tsmsbi  33135  dfufd2  33610  ccfldextdgrr  33816  issgon  34267  measbasedom  34346  oddpwdc  34498  eulerpartlemt  34515  ballotlem2  34633  ballotlemrinv  34678  bnj1533  34994  bnj983  35093  r1omhf  35249  r1omhfb  35256  fineqvomonb  35263  fineqvnttrclse  35268  r1omhfbregs  35281  fineqvr1ombregs  35282  0nn0m1nnn0  35295  lfuhgr3  35302  spthcycl  35311  satfv1  35545  satf0op  35559  fmla0xp  35565  fmla1  35569  elmsta  35730  antnestlaw1  35873  antnestlaw2  35874  antnestlaw3  35875  nepss  35900  dfon2  35972  distel  35983  fnimage  36109  altopthsn  36143  ellines  36334  rankeq1o  36353  opnrebl2  36503  df3nandALT1  36581  ttc00  36690  ttcwf  36706  ttcwf2  36707  ttcexbi  36715  ttc0el  36717  bj-animbi  36823  bj-dfbi6  36840  bj-consensus  36843  bj-falor2  36850  bj-bibibi  36851  bj-andnotim  36853  bj-alextruim  36931  bj-exextruan  36932  bj-ssbeq  36947  bj-19.41al  36953  bj-subst  36955  bj-eqs  36970  bj-cbvexw  36971  bj-sb  36984  bj-substax12  37021  bj-dfnnf3  37078  bj-equs45fv  37118  bj-hbaeb2  37125  bj-hbnaeb  37127  bj-equsal  37133  bj-sbsb  37144  bj-moeub  37156  bj-csbsnlem  37210  bj-snsetex  37270  bj-snglex  37280  bj-1uplth  37314  bj-1uplex  37315  bj-2uplth  37328  bj-2uplex  37329  bj-bm1.3ii  37371  bj-restpw  37404  bj-restuni  37409  bj-discrmoore  37423  bj-snmooreb  37426  bj-elid6  37484  bj-eldiag2  37491  mptsnunlem  37654  topdifinf  37665  elxp8  37687  finxp1o  37708  wl-moae  37841  wl-exeq  37859  wl-aleq  37860  wl-nfeqfb  37861  volsupnfl  37986  cover2  38036  isbnd3  38105  cntotbnd  38117  heibor  38142  isfld2  38326  isfldidl  38389  orfa  38403  eqbrb  38560  eqelb  38562  iss2  38665  issetssr  38904  n0el3  39057  detlem  39207  petlem  39236  eldisjs6  39261  prtlem16  39315  isltrn2N  40566  aks6d1c2p2  42558  aks6d1c6isolem3  42615  sn-iotalem  42662  dffltz  43067  eu6w  43109  3cubes  43122  ismrc  43133  isnacs3  43142  rexzrexnn0  43232  eldioph4b  43239  dford3  43456  wopprc  43458  ttac  43464  pw2f1ocnv  43465  dfac11  43490  dfac21  43494  isnumbasabl  43534  isnumbasgrp  43535  dfacbasgrp  43536  aaitgo  43590  dflim5  43757  nvocnvb  43849  dfno2  43855  ifpbi1b  43930  rp-fakeimass  43939  rp-fakeanorass  43940  rp-isfinite5  43944  rp-isfinite6  43945  dfsucon  43950  snen1g  43951  iscard4  43960  rtrclex  44044  cnvtrrel  44097  frege54cor0a  44290  isotone1  44475  isotone2  44476  gneispace  44561  k0004lem3  44576  grumnueq  44714  ismnushort  44728  nanorxor  44732  nzss  44744  pm10.55  44796  pm11.57  44816  pm13.192  44837  pm13.194  44839  ipo0  44875  ifr0  44876  xpexb  44880  3impexpbicom  44907  com3rgbi  44941  pm2.43bgbi  44944  pm2.43cbi  44945  sb5ALT  44952  trsbc  44967  2pm13.193  44979  ax6e2ndeq  44986  2uasbanh  44988  eelT01  45137  eel0T1  45138  uunT1  45206  zfregs2VD  45267  equncomVD  45294  trsbcVD  45303  undif3VD  45308  2pm13.193VD  45329  ax6e2eqVD  45333  ax6e2ndeqVD  45335  2uasbanhVD  45337  ax6e2ndeqALT  45357  tcfr  45390  mptssid  45670  elfzfzo  45710  allbutfi  45822  uzn0bi  45887  dvnprodlem3  46376  elaa2  46662  sge00  46804  elhoi  46970  ovn0  46994  ovolval4lem2  47078  confun  47387  afvfv0bi  47600  ffnafv  47619  afv2ndefb  47672  dfatafv2rnb  47675  afv2fv0b  47714  prpair  47961  sbcpr  47981  fpprel2  48217  sbgoldbmb  48262  vopnbgrelself  48331  isgrtri  48419  stgr1  48437  mgm2mgm  48703  nnpw2pb  49063  0aryfvalel  49110  mo0sn  49291  resinsnlem  49346  homf0  49484  isoval2  49510  oppccicb  49526  oppcciceq  49527  funcf2lem2  49557  initc  49566  isinito2  49974  isinito3  49975  termc  49994  dftermc3  50006  elsetrecs  50175  elpg  50189