Theorem impbii 210

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bicom  223  biid  262  2th  265  pm5.74  271  bitri  276  notnotb  316  con34b  317  notbi  320  bibi2i  338  con1b  359  con2b  360  bi2.04  388  imdi  390  pm4.8  393  pm4.81  394  impexp  451  ancom  461  anass  469  jcab  522  impimprbi  834  orcom  876  dfor2  907  oridm  910  orbi2i  918  or12  926  biorfriOLD  946  pm4.72  957  oibabs  959  jaob  969  pm4.44  1004  pm4.79  1011  andi  1015  pm4.82  1031  cases2ALT  1054  consensus  1058  3impexp  1365  3jaobOLD  1435  nanass  1517  tbw-bijust  1705  tbw-negdf  1706  19.26  1877  19.35  1884  19.21v  1946  19.23v  1949  19.41v  1956  19.3v  1989  19.9v  1991  equcom  2025  cbvalw  2042  alcomw  2052  excomw  2053  exexw  2060  sbbii  2087  sban  2091  sbv  2099  alcom  2170  19.3  2214  19.41  2247  sbalex  2254  sbalexOLD  2255  equsexv  2280  sbim  2314  cbvalv1  2349  cbval  2406  equsex  2426  aecom  2435  equs45f  2467  dfsb1  2489  dfsb2  2501  sb6f  2505  dfmoeu  2539  moabs  2547  mo3  2568  mo4  2570  exmoeu  2585  moanimlem  2622  euan  2625  euanv  2628  2mo  2652  2eu6  2660  euae  2663  axextb  2714  eqcom  2746  nebi  3014  r19.35  3097  r19.26  3099  r19.21v  3164  gencbvex  3488  gencbvex2  3489  pm13.183  3604  rr19.3v  3605  rr19.28v  3606  euxfr2w  3661  euxfr2  3663  reu6  3667  reu3  3668  reuan  3828  dfss2  3901  sspss  4033  complss  4081  unineq  4216  uneqin  4217  difrab  4246  sbnfc2  4367  un00  4373  ssdifeq0  4414  r19.2zb  4428  ralidmw  4444  ralidm  4445  pwidb  4550  snidb  4593  rabsnifsb  4654  tppreqb  4738  difsnb  4739  pwpw0  4744  sssn  4757  preq12b  4781  unissint  4902  uniintsn  4915  iununi  5028  al0ssb  5230  intex  5272  intnex  5273  axpweq  5279  iin0  5291  nfcvb  5305  eusvnfb  5322  eusv2nf  5324  ralxfrALT  5344  sspwb  5388  unipw  5389  opnz  5413  opth  5416  sbcop1  5428  opeqsng  5444  propeqop  5448  opthwiener  5455  opthhausdorff  5458  opthhausdorff0  5459  rexopabb  5470  ssopab2bw  5489  ssopab2b  5491  pwssun  5510  opelxp  5654  opthprc  5682  relsnb  5745  relop  5792  issetid  5796  xpid11  5874  elinxp  5971  eldmeldmressn  5977  iss  5987  iresn0n0  6006  asymref2  6067  xpnz  6110  xpdifid  6119  ssrnres  6129  dfrel2  6140  resssxp  6221  relrelss  6224  unixp0  6234  reuop  6244  dfpo2  6247  fn0  6616  funssxp  6683  f00  6709  f0bi  6710  dffo2  6743  f1o00  6802  fo00  6803  fv3  6845  dffn5  6885  dff2  7040  dff3  7041  dffo4  7044  dffo5  7045  exfo  7046  fmpt  7051  fompt  7059  ffnfv  7060  fsn  7077  fsn2  7078  funop  7092  funsneqopb  7095  fnsnbOLD  7110  isores1  7278  ssoprab2b  7425  eqoprab2bw  7426  eqfnov2  7486  unexb  7690  unexbOLD  7691  uniexb  7707  pwexb  7709  iunpw  7714  ordeleqon  7725  dford5  7727  onintrab  7739  ordsuc  7754  unon  7771  onuninsuci  7780  ordzsl  7785  onzsl  7786  f1oexbi  7868  ffoss  7888  1st2ndb  7971  frxp3  8091  suppssov1  8137  suppssov2  8138  suppssfv  8142  reldmtpos  8174  dfrecs3  8302  omopthi  8587  brinxper  8663  ecopover  8758  fsetexb  8801  mapsncnv  8831  mptelixpg  8873  elixpsn  8875  ixpsnf1o  8876  bren2  8920  en0  8955  en0ALT  8956  en0r  8957  en1  8961  en1b  8962  sbthb  9026  dom0  9033  canth2  9058  onfin2  9141  sdom1  9150  1sdom2dom  9154  fineqv  9167  unfilem1  9205  unfib  9209  pwfir  9217  pwfi  9219  fiint  9227  residfi  9238  unifpw  9255  wofib  9450  sucprcreg  9511  sucprcregOLD  9512  opthreg  9530  suc11reg  9531  infeq5  9549  rankwflemb  9708  r1elss  9721  pwwf  9722  unwf  9725  uniwf  9734  rankonid  9744  rankr1id  9777  rankuni  9778  rankxplim3  9796  scott0  9801  karden  9810  djuexb  9824  isnum3  9869  oncard  9875  card1  9883  cardlim  9887  cardmin2  9914  pm54.43lem  9915  ween  9948  acnnum  9965  alephsuc2  9993  alephgeom  9995  iscard3  10006  dfac3  10034  dfac4  10035  dfac5lem3  10038  dfac5  10042  dfac2  10045  dfac8  10049  dfac9  10050  dfacacn  10055  dfac13  10056  dfac12r  10060  dfac12k  10061  kmlem2  10065  kmlem13  10076  djuinf  10102  ackbij2  10155  cflim2  10176  isfin4-2  10227  isfin4p1  10228  isf33lem  10279  compsscnv  10284  fin1a2lem6  10318  domtriom  10356  ac9  10396  ac9s  10406  fodomb  10439  brdom3  10441  brdom5  10442  brdom4  10443  brdom7disj  10444  brdom6disj  10445  iunfo  10452  sdomsdomcard  10473  gch2  10589  gch3  10590  eltsk2g  10665  grutsk  10736  ordpipq  10856  ltbtwnnq  10892  mappsrpr  11022  map2psrpr  11024  elreal2  11046  le2tri3i  11267  elnn0nn  12470  elnnnn0b  12472  elnnnn0c  12473  elnnz  12525  elnn0z  12528  elz2  12533  elnnz1  12544  eluz2b2  12862  elnn1uz2  12866  elpqb  12917  elioo4g  13350  eluzfz2b  13478  fzn0  13483  elfz1end  13499  fzass4  13507  elfz1b  13538  nn0fz0  13570  fzolb  13611  fzon0  13623  elfzo0  13646  elfzo0z  13647  elfzo1  13658  fzo1fzo0n0  13661  om2uzrani  13905  nn0opthi  14223  hashkf  14285  isfinite4  14315  hashprb  14350  hashf1  14410  elss2prb  14441  iswrdb  14473  wrdexb  14478  0wrd0  14493  wrdl3s3  14915  cotr2g  14929  trclun  14967  rexanuz  15299  rexuz3  15302  fsum0diag  15730  fprod0diag  15942  divalgmod  16366  sadcp1  16415  isprm6  16675  nnoddn2prmb  16775  4sqlem4  16914  fnpr2ob  17513  mreunirn  17554  isdrs2  18263  isacs5  18505  isacs4  18506  isacs3  18507  dfgrp2  18929  dfgrp3  19006  dfgrp3e  19007  isnsg3  19126  gicer  19243  oppgmndb  19321  oppggrpb  19324  pmtrfb  19431  invghm  19799  isringrng  20259  opprrngb  20317  opprringb  20319  isnzr2hash  20491  isdomn4  20688  abvn0b  20808  gzrngunit  21408  dvdsrzring  21436  zringunit  21441  zlmlmod  21497  cygth  21546  frgpcyg  21548  zlmassa  21878  toprntopon  22908  tgclb  22953  iscldtop  23078  isnrm2  23341  isnrm3  23342  discmp  23381  dfconn2  23402  2ndcsb  23432  dis2ndc  23443  loclly  23470  unisngl  23510  locfindis  23513  iskgen2  23531  dfac14  23601  kqtop  23728  kqt0  23729  kqreg  23734  kqnrm  23735  hmpher  23767  hmphsymb  23769  hmph0  23778  kqhmph  23802  ist1-5lem  23803  elmptrab2  23811  isfil2  23839  filunirn  23865  isufil2  23891  hausflim  23964  isfcls  23992  alexsubALT  24034  istgp2  24074  ustbas  24210  xmetunirn  24320  dscmet  24555  dscopn  24556  isngp4  24595  zcld  24797  zlmclm  25097  iscmet2  25279  iundisj  25533  i1f1lem  25674  fta1b  26155  elply2  26179  elqaa  26306  aannenlem2  26313  wilth  27052  lgsne0  27316  2lgs  27388  2sqlem2  27399  ostth  27620  elno2  27636  bdayfo  27659  elons2  28268  eln0s2  28367  eln0s  28371  elzn0s  28408  eln0zs  28410  elnnzs  28411  remulscllem1  28510  mpteleeOLD  28982  wrdupgr  29172  wrdumgr  29184  umgrislfupgr  29210  uspgrupgrushgr  29266  usgrumgruspgr  29269  usgruspgrb  29270  usgrislfuspgr  29274  uvtx01vtx  29484  pthspthcyc  29889  wwlksnwwlksnon  30001  elwwlks2ons3  30041  clwwlkn1loopb  30131  eclclwwlkn1  30163  upgriseupth  30295  numclwwlkovh  30461  nmlno0lem  30882  isblo3i  30890  blocni  30894  hvsubeq0i  31152  hvaddcani  31154  bcseqi  31209  isch3  31330  norm1exi  31339  hhsssh  31358  shslubi  31474  dfch2  31496  pjoc1i  31520  pjchi  31521  shs00i  31539  chsscon3i  31550  chlejb1i  31565  chj00i  31576  shjshseli  31582  h1de2ctlem  31644  spanunsni  31668  cmcmi  31681  cmbr3i  31689  cmbr4i  31690  pj11i  31800  hosubeq0i  31915  dmadjrnb  31995  nmlnop0iALT  32084  lnopeq0i  32096  elunop2  32102  lnconi  32122  lncnopbd  32126  adjbdlnb  32173  adjbd1o  32174  adjeq0  32180  rnbra  32196  pjss1coi  32252  pjss2coi  32253  pjnormssi  32257  pjssdif2i  32263  pjssdif1i  32264  dfpjop  32271  pjinvari  32280  pjin2i  32282  pjci  32289  pjcmul1i  32290  pjcmul2i  32291  strb  32347  hstrbi  32355  mdsl1i  32410  atom1d  32442  chrelat2i  32454  cvbr4i  32456  cvexchi  32458  sumdmdi  32509  dmdbr4ati  32510  dmdbr5ati  32511  dmdbr6ati  32512  dmdbr7ati  32513  cdj3i  32530  eqtrb  32561  difeq  32606  iundisjf  32678  fpwrelmap  32825  iundisjfi  32888  xrge0tsmsbi  33155  dfufd2  33633  0mplrim  33698  ccfldextdgrr  33856  issgon  34307  measbasedom  34386  oddpwdc  34538  eulerpartlemt  34555  ballotlem2  34673  ballotlemrinv  34718  bnj1533  35034  bnj983  35133  r1omhf  35287  r1omhfb  35293  fineqvomonb  35300  fineqvnttrclse  35305  r1omhfbregs  35318  fineqvr1ombregs  35319  0nn0m1nnn0  35341  lfuhgr3  35348  spthcycl  35357  satfv1  35591  satf0op  35605  fmla0xp  35611  fmla1  35615  elmsta  35776  antnestlaw1  35919  antnestlaw2  35920  antnestlaw3  35921  nepss  35946  dfon2  36018  distel  36029  fnimage  36155  altopthsn  36189  ellines  36380  rankeq1o  36399  opnrebl2  36549  df3nandALT1  36627  ttc00  36736  ttcwf  36752  ttcwf2  36753  ttcexbi  36761  ttc0el  36763  bj-animbi  36869  bj-dfbi6  36886  bj-consensus  36889  bj-falor2  36896  bj-bibibi  36897  bj-andnotim  36899  bj-alextruim  36977  bj-exextruan  36978  bj-ssbeq  36993  bj-19.41al  36999  bj-subst  37001  bj-eqs  37016  bj-cbvexw  37017  bj-sb  37030  bj-substax12  37067  bj-dfnnf3  37124  bj-equs45fv  37164  bj-hbaeb2  37171  bj-hbnaeb  37173  bj-equsal  37179  bj-sbsb  37190  bj-moeub  37202  bj-csbsnlem  37256  bj-snsetex  37316  bj-snglex  37326  bj-1uplth  37360  bj-1uplex  37361  bj-2uplth  37374  bj-2uplex  37375  bj-bm1.3ii  37417  bj-restpw  37450  bj-restuni  37455  bj-discrmoore  37469  bj-snmooreb  37472  bj-elid6  37530  bj-eldiag2  37537  mptsnunlem  37700  topdifinf  37711  elxp8  37733  finxp1o  37754  wl-moae  37887  wl-exeq  37905  wl-aleq  37906  wl-nfeqfb  37907  volsupnfl  38032  cover2  38082  isbnd3  38151  cntotbnd  38163  heibor  38188  isfld2  38372  isfldidl  38435  orfa  38449  eqbrb  38606  eqelb  38608  iss2  38711  issetssr  38950  n0el3  39103  detlem  39253  petlem  39282  eldisjs6  39307  prtlem16  39361  isltrn2N  40612  aks6d1c2p2  42604  aks6d1c6isolem3  42661  sn-iotalem  42708  dffltz  43084  eu6w  43126  3cubes  43139  ismrc  43150  isnacs3  43159  rexzrexnn0  43249  eldioph4b  43256  dford3  43473  wopprc  43475  ttac  43481  pw2f1ocnv  43482  dfac11  43507  dfac21  43511  isnumbasabl  43551  isnumbasgrp  43552  dfacbasgrp  43553  aaitgo  43607  dflim5  43774  nvocnvb  43866  dfno2  43872  ifpbi1b  43947  rp-fakeimass  43956  rp-fakeanorass  43957  rp-isfinite5  43961  rp-isfinite6  43962  dfsucon  43967  snen1g  43968  iscard4  43977  rtrclex  44061  cnvtrrel  44114  frege54cor0a  44307  isotone1  44492  isotone2  44493  gneispace  44578  k0004lem3  44593  grumnueq  44731  ismnushort  44745  nanorxor  44749  nzss  44761  pm10.55  44813  pm11.57  44833  pm13.192  44854  pm13.194  44856  ipo0  44892  ifr0  44893  xpexb  44897  3impexpbicom  44924  com3rgbi  44958  pm2.43bgbi  44961  pm2.43cbi  44962  sb5ALT  44969  trsbc  44984  2pm13.193  44996  ax6e2ndeq  45003  2uasbanh  45005  eelT01  45154  eel0T1  45155  uunT1  45223  zfregs2VD  45284  equncomVD  45311  trsbcVD  45320  undif3VD  45325  2pm13.193VD  45346  ax6e2eqVD  45350  ax6e2ndeqVD  45352  2uasbanhVD  45354  ax6e2ndeqALT  45374  tcfr  45407  mptssid  45685  elfzfzo  45725  allbutfi  45837  uzn0bi  45902  dvnprodlem3  46391  elaa2  46677  sge00  46819  elhoi  46985  ovn0  47009  ovolval4lem2  47093  confun  47402  afvfv0bi  47615  ffnafv  47634  afv2ndefb  47687  dfatafv2rnb  47690  afv2fv0b  47729  prpair  47976  sbcpr  47996  fpprel2  48232  sbgoldbmb  48277  vopnbgrelself  48346  isgrtri  48434  stgr1  48452  mgm2mgm  48718  nnpw2pb  49078  0aryfvalel  49125  mo0sn  49306  resinsnlem  49361  homf0  49499  isoval2  49525  oppccicb  49541  oppcciceq  49542  funcf2lem2  49572  initc  49581  isinito2  49989  isinito3  49990  termc  50009  dftermc3  50021  elsetrecs  50190  elpg  50204