Theorem impbii 211

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bicom  224  biid  263  2th  266  pm5.74  272  bitri  277  notnotb  317  con34b  318  notbi  321  bibi2i  339  con1b  360  con2b  361  bi2.04  390  imdi  392  pm4.8  396  pm4.81  397  impexp  454  ancom  464  anass  472  jcab  525  abab  837  impimprbi  839  orcom  881  dfor2  912  oridm  915  orbi2i  923  or12  931  biorfriOLD  951  pm4.72  962  oibabs  964  jaob  974  pm4.44  1009  pm4.79  1016  andi  1020  pm4.82  1036  cases2ALT  1059  consensus  1063  3impexp  1371  3jaobOLD  1445  nanass  1529  tbw-bijust  1717  tbw-negdf  1718  19.26  1889  19.35  1896  19.21v  1958  19.23v  1961  19.41v  1968  19.3v  2001  19.9v  2003  equcom  2037  cbvalw  2054  alcomw  2064  excomw  2065  exexw  2072  dfsb  2092  sbbii  2108  sban  2112  sbv  2120  sbrimvw  2123  alcom  2192  19.3  2236  19.41  2269  sbalex  2276  sbalexOLD  2277  equsexv  2302  sbim  2336  cbvalv1  2371  cbval  2428  equsex  2448  aecom  2457  equs45f  2489  dfsb1  2511  dfsb2  2523  sb6f  2527  dfmoeu  2561  moabs  2569  mo3  2590  mo4  2592  exmoeu  2607  moanimlem  2644  euan  2647  euanv  2650  2mo  2674  2eu6  2682  euae  2685  axextb  2736  eqcom  2768  nebi  3036  r19.35  3119  r19.26  3121  r19.21v  3186  gencbvex  3509  gencbvex2  3510  pm13.183  3624  rr19.3v  3625  rr19.28v  3626  euxfr2w  3681  euxfr2  3683  reu6  3687  reu3  3688  reuan  3847  dfss2  3920  sspss  4053  complss  4102  unineq  4238  uneqin  4239  difrab  4268  sbnfc2  4390  un00  4396  ssdifeq0  4437  r19.2zb  4451  ralidmw  4467  ralidm  4468  pwidb  4574  snidb  4617  rabsnifsb  4678  tppreqb  4762  difsnb  4763  pwpw0  4768  sssn  4781  preq12b  4805  unissint  4927  uniintsn  4940  iununi  5053  al0ssb  5255  intex  5297  intnex  5298  axpweq  5304  iin0  5316  nfcvb  5330  eusvnfb  5347  eusv2nf  5349  ralxfrALT  5369  sspwb  5413  unipw  5414  opnz  5438  opth  5441  sbcop1  5453  opeqsng  5469  propeqop  5473  opthwiener  5480  opthhausdorff  5483  opthhausdorff0  5484  rexopabb  5495  ssopab2bw  5514  ssopab2b  5516  pwssun  5535  opelxp  5679  opthprc  5707  relsnb  5771  relop  5818  issetid  5822  xpid11  5904  elinxp  6001  eldmeldmressn  6007  iss  6020  iresn0n0  6039  asymref2  6100  xpnz  6140  xpdifid  6149  ssrnres  6159  dfrel2  6170  resssxp  6252  relrelss  6255  unixp0  6265  reuop  6275  dfpo2  6278  fn0  6647  funssxp  6715  f00  6741  f0bi  6742  dffo2  6777  f1o00  6837  fo00  6838  fv3  6880  dffn5  6920  dff2  7075  dff3  7076  dffo4  7079  dffo5  7080  exfo  7081  fmpt  7086  fompt  7094  ffnfv  7095  fsn  7112  fsn2  7113  funop  7127  funsneqopb  7130  fnsnbOLD  7145  isores1  7313  ssoprab2b  7460  eqoprab2bw  7461  eqfnov2  7521  unexb  7725  unexbOLD  7726  uniexb  7742  pwexb  7744  iunpw  7749  ordeleqon  7760  dford5  7762  onintrab  7774  ordsuc  7789  unon  7806  onuninsuci  7815  ordzsl  7820  onzsl  7821  f1oexbi  7904  ffoss  7922  1st2ndb  8005  frxp3  8125  suppssov1  8171  suppssov2  8172  suppssfv  8176  reldmtpos  8208  dfrecs3  8337  omopthi  8625  brinxper  8702  ecopover  8797  fsetexb  8839  mapsncnv  8869  mptelixpg  8911  elixpsn  8913  ixpsnf1o  8914  bren2  8958  en0  8993  en0ALT  8994  en0r  8995  en1  8999  en1b  9000  sbthb  9064  dom0  9071  canth2  9096  onfin2  9179  sdom1  9188  1sdom2dom  9192  fineqv  9205  unfilem1  9243  unfib  9247  pwfir  9255  pwfi  9257  fiint  9265  residfi  9275  unifpw  9292  wofib  9487  sucprcreg  9548  sucprcregOLD  9549  opthreg  9567  suc11reg  9568  infeq5  9586  rankwflemb  9745  r1elss  9758  pwwf  9759  unwf  9762  uniwf  9771  rankonid  9781  rankr1id  9814  rankuni  9815  rankxplim3  9833  scott0  9838  karden  9847  djuexb  9861  isnum3  9906  oncard  9912  card1  9920  cardlim  9924  cardmin2  9951  pm54.43lem  9952  ween  9985  acnnum  10002  alephsuc2  10030  alephgeom  10032  iscard3  10043  dfac3  10071  dfac4  10072  dfac5lem3  10075  dfac5  10079  dfac2  10082  dfac8  10086  dfac9  10087  dfacacn  10092  dfac13  10093  dfac12r  10097  dfac12k  10098  kmlem2  10102  kmlem13  10113  djuinf  10139  ackbij2  10192  cflim2  10214  isfin4-2  10265  isfin4p1  10266  isf33lem  10317  compsscnv  10322  fin1a2lem6  10356  domtriom  10394  ac9  10434  ac9s  10444  fodomb  10477  brdom3  10479  brdom5  10480  brdom4  10481  brdom7disj  10482  brdom6disj  10483  iunfo  10490  sdomsdomcard  10511  gch2  10627  gch3  10628  eltsk2g  10703  grutsk  10774  ordpipq  10894  ltbtwnnq  10930  mappsrpr  11060  map2psrpr  11062  elreal2  11084  le2tri3i  11307  elnn0nn  12517  elnnnn0b  12519  elnnnn0c  12520  elnnz  12572  elnn0z  12575  elz2  12580  elnnz1  12591  eluz2b2  12916  elnn1uz2  12920  elpqb  12971  elioo4g  13404  eluzfz2b  13532  fzn0  13537  elfz1end  13553  fzass4  13561  elfz1b  13592  nn0fz0  13624  fzolb  13665  fzon0  13677  elfzo0  13700  elfzo0z  13701  elfzo1  13712  fzo1fzo0n0  13715  om2uzrani  13959  nn0opthi  14277  hashkf  14339  isfinite4  14369  hashprb  14404  hashf1  14464  elss2prb  14495  iswrdb  14527  wrdexb  14532  0wrd0  14547  wrdl3s3  14969  cotr2g  14983  trclun  15021  rexanuz  15364  rexuz3  15367  fsum0diag  15795  fprod0diag  16007  divalgmod  16431  sadcp1  16480  isprm6  16740  nnoddn2prmb  16840  4sqlem4  16979  fnpr2ob  17579  mreunirn  17620  isdrs2  18329  isacs5  18571  isacs4  18572  isacs3  18573  dfgrp2  18995  dfgrp3  19072  dfgrp3e  19073  isnsg3  19192  gicer  19308  oppgmndb  19386  oppggrpb  19389  pmtrfb  19496  invghm  19864  isringrng  20324  opprrngb  20382  opprringb  20384  isnzr2hash  20556  isdomn4  20753  abvn0b  20873  gzrngunit  21473  dvdsrzring  21501  zringunit  21506  zlmlmod  21562  cygth  21611  frgpcyg  21613  zlmassa  21943  toprntopon  22973  tgclb  23018  iscldtop  23143  isnrm2  23406  isnrm3  23407  discmp  23446  dfconn2  23467  2ndcsb  23497  dis2ndc  23508  loclly  23535  unisngl  23575  locfindis  23578  iskgen2  23596  dfac14  23666  kqtop  23793  kqt0  23794  kqreg  23799  kqnrm  23800  hmpher  23832  hmphsymb  23834  hmph0  23843  kqhmph  23867  ist1-5lem  23868  elmptrab2  23876  isfil2  23904  filunirn  23930  isufil2  23956  hausflim  24029  isfcls  24057  alexsubALT  24099  istgp2  24139  ustbas  24275  xmetunirn  24385  dscmet  24620  dscopn  24621  isngp4  24660  zcld  24862  zlmclm  25162  iscmet2  25344  iundisj  25598  i1f1lem  25739  fta1b  26220  elply2  26244  elqaa  26374  aannenlem2  26381  wilth  27123  lgsne0  27387  2lgs  27459  2sqlem2  27470  ostth  27691  elno2  27706  bdayfo  27729  elons2  28339  eln0s2  28438  eln0s  28442  elzn0s  28479  eln0zs  28481  elnnzs  28482  remulscllem1  28581  mpteleeOLD  29053  wrdupgr  29243  wrdumgr  29255  umgrislfupgr  29281  uspgrupgrushgr  29337  usgrumgruspgr  29340  usgruspgrb  29341  usgrislfuspgr  29345  uvtx01vtx  29555  pthspthcyc  29960  wwlksnwwlksnon  30072  elwwlks2ons3  30112  clwwlkn1loopb  30202  eclclwwlkn1  30234  upgriseupth  30366  numclwwlkovh  30532  nmlno0lem  30953  isblo3i  30961  blocni  30965  hvsubeq0i  31223  hvaddcani  31225  bcseqi  31280  isch3  31401  norm1exi  31410  hhsssh  31429  shslubi  31545  dfch2  31567  pjoc1i  31591  pjchi  31592  shs00i  31610  chsscon3i  31621  chlejb1i  31636  chj00i  31647  shjshseli  31653  h1de2ctlem  31715  spanunsni  31739  cmcmi  31752  cmbr3i  31760  cmbr4i  31761  pj11i  31871  hosubeq0i  31986  dmadjrnb  32066  nmlnop0iALT  32155  lnopeq0i  32167  elunop2  32173  lnconi  32193  lncnopbd  32197  adjbdlnb  32244  adjbd1o  32245  adjeq0  32251  rnbra  32267  pjss1coi  32323  pjss2coi  32324  pjnormssi  32328  pjssdif2i  32334  pjssdif1i  32335  dfpjop  32342  pjinvari  32351  pjin2i  32353  pjci  32360  pjcmul1i  32361  pjcmul2i  32362  strb  32418  hstrbi  32426  mdsl1i  32481  atom1d  32513  chrelat2i  32525  cvbr4i  32527  cvexchi  32529  sumdmdi  32580  dmdbr4ati  32581  dmdbr5ati  32582  dmdbr6ati  32583  dmdbr7ati  32584  cdj3i  32601  eqtrb  32632  difeq  32677  iundisjf  32749  fpwrelmap  32896  iundisjfi  32959  xrge0tsmsbi  33215  dflring2  33650  dfufd2  33707  0mplrim  33772  ccfldextdgrr  33930  issgon  34381  measbasedom  34460  oddpwdc  34612  eulerpartlemt  34629  ballotlem2  34747  ballotlemrinv  34792  bnj1533  35108  bnj983  35207  r1omhf  35363  r1omhfb  35369  fineqvomonb  35376  fineqvnttrclse  35381  r1omhfbregs  35394  fineqvr1ombregs  35395  0nn0m1nnn0  35424  lfuhgr3  35431  spthcycl  35440  satfv1  35674  satf0op  35688  fmla0xp  35694  fmla1  35698  elmsta  35859  antnestlaw1  36002  antnestlaw2  36003  antnestlaw3  36004  nepss  36029  dfon2  36101  distel  36112  fnimage  36238  altopthsn  36272  ellines  36463  rankeq1o  36482  opnrebl2  36642  df3nandALT1  36720  ttc00  36829  ttcwf  36845  ttcwf2  36846  ttcexbi  36854  ttc0el  36856  bj-animbi  36962  bj-dfbi6  36979  bj-consensus  36982  bj-falor2  36989  bj-bibibi  36990  bj-andnotim  36992  bj-alextruim  37070  bj-exextruan  37071  bj-ssbeq  37086  bj-19.41al  37092  bj-subst  37094  bj-eqs  37109  bj-cbvexw  37110  bj-sb  37123  bj-substax12  37160  bj-dfnnf3  37217  bj-equs45fv  37257  bj-hbaeb2  37264  bj-hbnaeb  37266  bj-equsal  37272  bj-sbsb  37283  bj-moeub  37295  bj-csbsnlem  37349  bj-snsetex  37409  bj-snglex  37419  bj-1uplth  37453  bj-1uplex  37454  bj-2uplth  37467  bj-2uplex  37468  bj-bm1.3ii  37510  bj-restpw  37543  bj-restuni  37548  bj-discrmoore  37562  bj-snmooreb  37565  bj-elid6  37623  bj-eldiag2  37630  mptsnunlem  37793  topdifinf  37804  elxp8  37826  finxp1o  37847  wl-moae  37980  wl-exeq  37998  wl-aleq  37999  wl-nfeqfb  38000  volsupnfl  38125  cover2  38175  isbnd3  38244  cntotbnd  38256  heibor  38281  isfld2  38465  isfldidl  38528  orfa  38542  eqbrb  38699  eqelb  38701  iss2  38804  issetssr  39043  n0el3  39196  detlem  39346  petlem  39375  eldisjs6  39400  prtlem16  39454  isltrn2N  40705  aks6d1c2p2  42697  aks6d1c6isolem3  42754  sn-iotalem  42801  dffltz  43177  eu6w  43219  3cubes  43232  ismrc  43243  isnacs3  43252  rexzrexnn0  43342  eldioph4b  43349  dford3  43566  wopprc  43568  ttac  43574  pw2f1ocnv  43575  dfac11  43600  dfac21  43604  isnumbasabl  43644  isnumbasgrp  43645  dfacbasgrp  43646  aaitgo  43700  dflim5  43867  nvocnvb  43959  dfno2  43965  ifpbi1b  44040  rp-fakeimass  44049  rp-fakeanorass  44050  rp-isfinite5  44054  rp-isfinite6  44055  dfsucon  44060  snen1g  44061  iscard4  44070  rtrclex  44154  cnvtrrel  44207  frege54cor0a  44400  isotone1  44585  isotone2  44586  gneispace  44671  k0004lem3  44686  grumnueq  44824  ismnushort  44838  nanorxor  44842  nzss  44854  pm10.55  44906  pm11.57  44926  pm13.192  44947  pm13.194  44949  ipo0  44985  ifr0  44986  xpexb  44990  3impexpbicom  45017  com3rgbi  45051  pm2.43bgbi  45054  pm2.43cbi  45055  sb5ALT  45062  trsbc  45077  2pm13.193  45089  ax6e2ndeq  45096  2uasbanh  45098  eelT01  45247  eel0T1  45248  uunT1  45316  zfregs2VD  45377  equncomVD  45404  trsbcVD  45413  undif3VD  45418  2pm13.193VD  45439  ax6e2eqVD  45443  ax6e2ndeqVD  45445  2uasbanhVD  45447  ax6e2ndeqALT  45467  tcfr  45500  mptssid  45777  elfzfzo  45817  allbutfi  45929  uzn0bi  45994  dvnprodlem3  46483  elaa2  46769  sge00  46911  elhoi  47077  ovn0  47101  ovolval4lem2  47185  confun  47494  afvfv0bi  47707  ffnafv  47726  afv2ndefb  47779  dfatafv2rnb  47782  afv2fv0b  47821  prpair  48068  sbcpr  48088  fpprel2  48324  sbgoldbmb  48369  vopnbgrelself  48438  isgrtri  48526  stgr1  48544  mgm2mgm  48810  nnpw2pb  49170  0aryfvalel  49217  mo0sn  49398  resinsnlem  49453  homf0  49591  isoval2  49617  oppccicb  49633  oppcciceq  49634  funcf2lem2  49664  initc  49673  isinito2  50081  isinito3  50082  termc  50101  dftermc3  50113  elsetrecs  50282  elpg  50296