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  1511  tbw-bijust  1699  tbw-negdf  1700  19.26  1871  19.35  1878  19.21v  1940  19.23v  1943  19.41v  1950  19.3v  1983  19.9v  1985  equcom  2019  cbvalw  2036  alcomw  2046  excomw  2047  exexw  2054  sbbii  2079  sban  2083  sbv  2091  alcom  2162  19.3  2205  19.41  2238  sbalex  2245  sbalexOLD  2246  equsexv  2271  sbim  2305  cbvalv1  2341  cbval  2398  equsex  2418  aecom  2427  equs45f  2459  dfsb1  2481  dfsb2  2493  sb6f  2497  dfmoeu  2531  moabs  2538  mobii  2543  mo3  2559  mo4  2561  exmoeu  2576  moanimlem  2613  euan  2616  euanv  2619  2mo  2643  2eu6  2652  euae  2655  axextb  2706  eqcom  2738  nebi  3008  r19.35  3090  r19.26  3092  r19.21v  3157  gencbvex  3495  gencbvex2  3496  pm13.183  3616  rr19.3v  3617  rr19.28v  3618  euxfr2w  3674  euxfr2  3676  reu6  3680  reu3  3681  reuan  3842  dfss2  3915  sspss  4047  complss  4096  unineq  4233  uneqin  4234  difrab  4263  ab0w  4324  sbnfc2  4384  un00  4390  ssdifeq0  4432  r19.2zb  4441  ralidmw  4453  ralidm  4457  ralf0  4459  pwidb  4566  snidb  4609  rabsnifsb  4670  tppreqb  4752  difsnb  4753  pwpw0  4760  sssn  4773  preq12b  4797  unissint  4917  uniintsn  4930  iununi  5042  al0ssb  5241  intex  5277  intnex  5278  axpweq  5284  iin0  5295  nfcvb  5309  eusvnfb  5326  eusv2nf  5328  ralxfrALT  5348  sspwb  5385  unipw  5386  opnz  5408  opth  5411  sbcop1  5423  opeqsng  5438  propeqop  5442  opthwiener  5449  opthhausdorff  5452  opthhausdorff0  5453  rexopabb  5463  ssopab2bw  5482  ssopab2b  5484  pwssun  5503  opelxp  5647  opthprc  5675  relsnb  5737  relop  5785  issetid  5789  xpid11  5867  elinxp  5963  eldmeldmressn  5969  iss  5979  iresn0n0  5998  asymref2  6059  xpnz  6101  xpdifid  6110  ssrnres  6120  dfrel2  6131  resssxp  6212  relrelss  6215  unixp0  6225  reuop  6235  dfpo2  6238  fn0  6607  funssxp  6674  f00  6700  f0bi  6701  dffo2  6734  f1o00  6793  fo00  6794  fv3  6835  dffn5  6875  dff2  7027  dff3  7028  dffo4  7031  dffo5  7032  exfo  7033  fmpt  7038  fompt  7046  ffnfv  7047  fsn  7063  fsn2  7064  funop  7077  funsneqopb  7080  fnsnbOLD  7095  isores1  7263  ssoprab2b  7410  eqoprab2bw  7411  eqfnov2  7471  unexb  7675  unexbOLD  7676  uniexb  7692  pwexb  7694  iunpw  7699  ordeleqon  7710  dford5  7712  onintrab  7724  ordsuc  7739  unon  7756  onuninsuci  7765  ordzsl  7770  onzsl  7771  f1oexbi  7853  ffoss  7873  1st2ndb  7956  frxp3  8076  suppssov1  8122  suppssov2  8123  suppssfv  8127  reldmtpos  8159  dfrecs3  8287  omopthi  8571  brinxper  8646  ecopover  8740  fsetexb  8783  mapsncnv  8812  mptelixpg  8854  elixpsn  8856  ixpsnf1o  8857  bren2  8900  en0  8935  en0ALT  8936  en0r  8937  en1  8941  en1b  8942  sbthb  9006  dom0  9013  canth2  9038  onfin2  9120  sdom1  9129  1sdom2dom  9133  fineqv  9146  unfilem1  9184  unfib  9188  pwfir  9196  pwfi  9198  fiint  9206  residfi  9217  unifpw  9234  wofib  9426  sucprcreg  9485  opthreg  9503  suc11reg  9504  infeq5  9522  rankwflemb  9681  r1elss  9694  pwwf  9695  unwf  9698  uniwf  9707  rankonid  9717  rankr1id  9750  rankuni  9751  rankxplim3  9769  scott0  9774  karden  9783  djuexb  9797  isnum3  9842  oncard  9848  card1  9856  cardlim  9860  cardmin2  9887  pm54.43lem  9888  ween  9921  acnnum  9938  alephsuc2  9966  alephgeom  9968  iscard3  9979  dfac3  10007  dfac4  10008  dfac5lem3  10011  dfac5  10015  dfac2  10018  dfac8  10022  dfac9  10023  dfacacn  10028  dfac13  10029  dfac12r  10033  dfac12k  10034  kmlem2  10038  kmlem13  10049  djuinf  10075  ackbij2  10128  cflim2  10149  isfin4-2  10200  isfin4p1  10201  isf33lem  10252  compsscnv  10257  fin1a2lem6  10291  domtriom  10329  ac9  10369  ac9s  10379  fodomb  10412  brdom3  10414  brdom5  10415  brdom4  10416  brdom7disj  10417  brdom6disj  10418  iunfo  10425  sdomsdomcard  10446  gch2  10561  gch3  10562  eltsk2g  10637  grutsk  10708  ordpipq  10828  ltbtwnnq  10864  mappsrpr  10994  map2psrpr  10996  elreal2  11018  le2tri3i  11238  elnn0nn  12418  elnnnn0b  12420  elnnnn0c  12421  elnnz  12473  elnn0z  12476  elz2  12481  elnnz1  12493  eluz2b2  12814  elnn1uz2  12818  elpqb  12869  elioo4g  13301  eluzfz2b  13428  fzn0  13433  elfz1end  13449  fzass4  13457  elfz1b  13488  nn0fz0  13520  fzolb  13560  fzon0  13572  elfzo0  13595  elfzo0z  13596  elfzo1  13607  fzo1fzo0n0  13610  om2uzrani  13854  nn0opthi  14172  hashkf  14234  isfinite4  14264  hashprb  14299  hashf1  14359  elss2prb  14390  iswrdb  14422  wrdexb  14427  0wrd0  14442  wrdl3s3  14864  cotr2g  14878  trclun  14916  rexanuz  15248  rexuz3  15251  fsum0diag  15679  fprod0diag  15888  divalgmod  16312  sadcp1  16361  isprm6  16620  nnoddn2prmb  16720  4sqlem4  16859  fnpr2ob  17457  mreunirn  17498  isdrs2  18207  isacs5  18449  isacs4  18450  isacs3  18451  dfgrp2  18870  dfgrp3  18947  dfgrp3e  18948  isnsg3  19067  gicer  19184  oppgmndb  19262  oppggrpb  19265  pmtrfb  19372  invghm  19740  isringrng  20200  opprrngb  20259  opprringb  20261  isnzr2hash  20429  isdomn4  20626  abvn0b  20746  gzrngunit  21365  dvdsrzring  21393  zringunit  21398  zlmlmod  21454  cygth  21503  frgpcyg  21505  zlmassa  21835  toprntopon  22835  tgclb  22880  iscldtop  23005  isnrm2  23268  isnrm3  23269  discmp  23308  dfconn2  23329  2ndcsb  23359  dis2ndc  23370  loclly  23397  unisngl  23437  locfindis  23440  iskgen2  23458  dfac14  23528  kqtop  23655  kqt0  23656  kqreg  23661  kqnrm  23662  hmpher  23694  hmphsymb  23696  hmph0  23705  kqhmph  23729  ist1-5lem  23730  elmptrab2  23738  isfil2  23766  filunirn  23792  isufil2  23818  hausflim  23891  isfcls  23919  alexsubALT  23961  istgp2  24001  ustbas  24137  xmetunirn  24247  dscmet  24482  dscopn  24483  isngp4  24522  zcld  24724  zlmclm  25034  iscmet2  25216  iundisj  25471  i1f1lem  25612  fta1b  26099  elply2  26123  elqaa  26252  aannenlem2  26259  wilth  27003  lgsne0  27268  2lgs  27340  2sqlem2  27351  ostth  27572  elno2  27588  bdayfo  27611  elons2  28190  eln0s  28282  elzn0s  28317  eln0zs  28319  elnnzs  28320  remulscllem1  28397  mptelee  28868  wrdupgr  29058  wrdumgr  29070  umgrislfupgr  29096  uspgrupgrushgr  29152  usgrumgruspgr  29155  usgruspgrb  29156  usgrislfuspgr  29160  uvtx01vtx  29370  pthspthcyc  29776  wwlksnwwlksnon  29888  elwwlks2ons3  29928  clwwlkn1loopb  30015  eclclwwlkn1  30047  upgriseupth  30179  numclwwlkovh  30345  nmlno0lem  30765  isblo3i  30773  blocni  30777  hvsubeq0i  31035  hvaddcani  31037  bcseqi  31092  isch3  31213  norm1exi  31222  hhsssh  31241  shslubi  31357  dfch2  31379  pjoc1i  31403  pjchi  31404  shs00i  31422  chsscon3i  31433  chlejb1i  31448  chj00i  31459  shjshseli  31465  h1de2ctlem  31527  spanunsni  31551  cmcmi  31564  cmbr3i  31572  cmbr4i  31573  pj11i  31683  hosubeq0i  31798  dmadjrnb  31878  nmlnop0iALT  31967  lnopeq0i  31979  elunop2  31985  lnconi  32005  lncnopbd  32009  adjbdlnb  32056  adjbd1o  32057  adjeq0  32063  rnbra  32079  pjss1coi  32135  pjss2coi  32136  pjnormssi  32140  pjssdif2i  32146  pjssdif1i  32147  dfpjop  32154  pjinvari  32163  pjin2i  32165  pjci  32172  pjcmul1i  32173  pjcmul2i  32174  strb  32230  hstrbi  32238  mdsl1i  32293  atom1d  32325  chrelat2i  32337  cvbr4i  32339  cvexchi  32341  sumdmdi  32392  dmdbr4ati  32393  dmdbr5ati  32394  dmdbr6ati  32395  dmdbr7ati  32396  cdj3i  32413  eqtrb  32445  difeq  32490  iundisjf  32561  fpwrelmap  32708  iundisjfi  32770  xrge0tsmsbi  33035  dfufd2  33507  ccfldextdgrr  33677  issgon  34128  measbasedom  34207  oddpwdc  34359  eulerpartlemt  34376  ballotlem2  34494  ballotlemrinv  34539  bnj1533  34856  bnj983  34955  r1omhf  35109  r1omhfb  35115  r1omhfbregs  35125  fineqvr1ombregs  35127  fineqvnttrclse  35136  0nn0m1nnn0  35149  lfuhgr3  35156  spthcycl  35165  satfv1  35399  satf0op  35413  fmla0xp  35419  fmla1  35423  elmsta  35584  antnestlaw1  35727  antnestlaw2  35728  antnestlaw3  35729  nepss  35754  dfon2  35826  distel  35837  fnimage  35963  altopthsn  35995  ellines  36186  rankeq1o  36205  opnrebl2  36355  df3nandALT1  36433  bj-animbi  36593  bj-dfbi6  36609  bj-consensus  36612  bj-falor2  36619  bj-bibibi  36620  bj-andnotim  36622  bj-cbval  36683  bj-cbvex  36684  bj-ssbeq  36687  bj-19.41al  36693  bj-subst  36695  bj-eqs  36709  bj-cbvexw  36710  bj-sb  36721  bj-substax12  36755  bj-dfnnf3  36791  bj-equs45fv  36845  bj-hbaeb2  36852  bj-hbnaeb  36854  bj-equsal  36860  bj-sbsb  36871  bj-moeub  36883  bj-csbsnlem  36937  bj-snsetex  36997  bj-snglex  37007  bj-1uplth  37041  bj-1uplex  37042  bj-2uplth  37055  bj-2uplex  37056  bj-bm1.3ii  37098  bj-restpw  37126  bj-restuni  37131  bj-discrmoore  37145  bj-snmooreb  37148  bj-elid6  37204  bj-eldiag2  37211  mptsnunlem  37372  topdifinf  37383  elxp8  37405  finxp1o  37426  wl-moae  37550  wl-exeq  37568  wl-aleq  37569  wl-nfeqfb  37570  wl-ax11-lem6  37624  volsupnfl  37705  cover2  37755  isbnd3  37824  cntotbnd  37836  heibor  37861  isfld2  38045  isfldidl  38108  orfa  38122  eqbrb  38267  eqelb  38269  iss2  38372  issetssr  38540  n0el3  38689  detlem  38821  petlem  38850  prtlem16  38908  isltrn2N  40159  aks6d1c2p2  42152  aks6d1c6isolem3  42209  sn-iotalem  42254  dffltz  42667  eu6w  42709  3cubes  42723  ismrc  42734  isnacs3  42743  rexzrexnn0  42837  eldioph4b  42844  dford3  43061  wopprc  43063  ttac  43069  pw2f1ocnv  43070  dfac11  43095  dfac21  43099  isnumbasabl  43139  isnumbasgrp  43140  dfacbasgrp  43141  aaitgo  43195  dflim5  43362  nvocnvb  43455  dfno2  43461  ifpbi1b  43536  rp-fakeimass  43545  rp-fakeanorass  43546  rp-isfinite5  43550  rp-isfinite6  43551  dfsucon  43556  snen1g  43557  iscard4  43566  rtrclex  43650  cnvtrrel  43703  frege54cor0a  43896  isotone1  44081  isotone2  44082  gneispace  44167  k0004lem3  44182  grumnueq  44320  ismnushort  44334  nanorxor  44338  nzss  44350  pm10.55  44402  pm11.57  44422  pm13.192  44443  pm13.194  44445  ipo0  44481  ifr0  44482  xpexb  44486  3impexpbicom  44513  com3rgbi  44547  pm2.43bgbi  44550  pm2.43cbi  44551  sb5ALT  44558  trsbc  44573  2pm13.193  44585  ax6e2ndeq  44592  2uasbanh  44594  eelT01  44743  eel0T1  44744  uunT1  44812  zfregs2VD  44873  equncomVD  44900  trsbcVD  44909  undif3VD  44914  2pm13.193VD  44935  ax6e2eqVD  44939  ax6e2ndeqVD  44941  2uasbanhVD  44943  ax6e2ndeqALT  44963  tcfr  44996  mptssid  45278  elfzfzo  45318  allbutfi  45431  uzn0bi  45497  dvnprodlem3  45986  elaa2  46272  sge00  46414  elhoi  46580  ovn0  46604  ovolval4lem2  46688  confun  46970  afvfv0bi  47183  ffnafv  47202  afv2ndefb  47255  dfatafv2rnb  47258  afv2fv0b  47297  prpair  47532  sbcpr  47552  fpprel2  47772  sbgoldbmb  47817  vopnbgrelself  47886  isgrtri  47974  stgr1  47992  mgm2mgm  48258  nnpw2pb  48619  0aryfvalel  48666  mo0sn  48847  resinsnlem  48902  homf0  49041  isoval2  49067  oppccicb  49083  oppcciceq  49084  funcf2lem2  49114  initc  49123  isinito2  49531  isinito3  49532  termc  49551  dftermc3  49563  elsetrecs  49732  elpg  49746