Theorem impbii 212

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicom  225  biid  264  2th  267  pm5.74  273  bitri  278  notnotb  318  con34b  319  notbi  322  bibi2i  340  con1b  361  con2b  362  bi2.04  392  imdi  394  pm4.8  398  pm4.81  399  impexp  456  ancom  466  anass  474  jcab  527  abab  840  impimprbi  842  orcom  884  dfor2  915  oridm  918  orbi2i  926  or12  934  pm4.72  964  oibabs  966  jaob  976  pm4.44  1012  pm4.79  1021  andi  1025  pm4.82  1041  cases2ALT  1064  consensus  1068  3impexp  1377  nanass  1540  tbw-bijust  1731  tbw-negdf  1732  19.26  1903  19.35  1910  19.21v  1972  19.23v  1975  19.41v  1982  19.3v  2015  19.9v  2017  equcom  2051  cbvalw  2068  alcomw  2078  excomw  2079  exexw  2086  sbbii  2113  sban  2117  sbv  2125  sbrimvw  2128  alcom  2197  19.3  2241  19.41  2274  sbalex  2281  equsexv  2306  sbim  2340  cbvalv1  2375  cbval  2432  equsex  2452  aecom  2461  equs45f  2493  dfsb1  2515  dfsb2  2527  sb6f  2531  dfmoeu  2565  moabs  2573  mo3  2594  mo4  2596  exmoeu  2611  moanimlem  2648  euan  2651  euanv  2654  2mo  2678  2eu6  2686  euae  2689  axextb  2740  eqcom  2772  nebi  3040  r19.35  3125  r19.26  3127  r19.21v  3192  gencbvex  3513  gencbvex2  3514  pm13.183  3627  rr19.3v  3628  rr19.28v  3629  euxfr2w  3685  euxfr2  3687  reu6  3691  reu3  3692  reuan  3851  dfss2  3924  sspss  4057  complss  4105  unineq  4241  uneqin  4242  difrab  4271  un00  4364  vvin  4366  sbnfc2  4404  ssdifeq0  4449  r19.2zb  4463  ralidmw  4479  ralidm  4480  pwidb  4586  snidb  4629  rabsnifsb  4690  tppreqb  4775  difsnb  4776  pwpw0  4781  sssn  4794  preq12b  4817  unissint  4939  uniintsn  4952  iununi  5067  al0ssb  5273  intex  5316  intnex  5317  axpweq  5323  iin0  5335  nfcvb  5349  eusvnfb  5366  eusv2nf  5368  ralxfrALT  5388  sspwb  5432  unipw  5433  opnz  5457  opth  5460  sbcop1  5472  opeqsng  5488  propeqop  5492  opthwiener  5499  opthhausdorff  5502  opthhausdorff0  5503  rexopabb  5514  ssopab2bw  5534  ssopab2b  5536  pwssun  5555  opelxp  5699  opthprc  5727  relsnb  5791  relop  5838  issetid  5842  xpid11  5924  elinxp  6020  eldmeldmressn  6026  iss  6039  iresn0n0  6058  asymref2  6119  xpnz  6158  xpdifid  6167  xpdifcnvepel  6168  ssrnres  6178  dfrel2  6189  relcnvtrg  6270  resssxp  6274  relrelss  6277  unixp0  6288  reuop  6298  dfpo2  6301  fn0  6670  funssxp  6738  f00  6764  f0bi  6765  dffo2  6800  f1o00  6860  fo00  6861  fv3  6903  dffn5  6943  dff2  7098  dff3  7099  dffo4  7102  dffo5  7103  exfo  7104  fmpt  7109  fompt  7117  ffnfv  7118  fsn  7135  fsn2  7136  funop  7150  funsneqopb  7153  fnsnbOLD  7168  isores1  7338  ssoprab2b  7485  eqoprab2bw  7486  eqfnov2  7546  unexb  7750  uniexb  7765  pwexb  7767  iunpw  7772  ordeleqon  7783  dford5  7785  onintrab  7797  ordsuc  7812  unon  7829  onuninsuci  7838  ordzsl  7843  onzsl  7844  f1oexbi  7927  ffoss  7945  1st2ndb  8028  frxp3  8149  suppssov1  8195  suppssov2  8196  suppssfv  8200  reldmtpos  8232  dfrecs3  8361  omopthi  8649  brinxper  8726  ecopover  8821  fsetexb  8863  mapsncnv  8893  mptelixpg  8935  elixpsn  8937  ixpsnf1o  8938  bren2  8982  en0  9017  en0ALT  9018  en0r  9019  en1  9023  en1b  9024  sbthb  9089  dom0  9096  canth2  9121  onfin2  9204  sdom1  9213  1sdom2dom  9217  fineqv  9230  unfilem1  9268  unfib  9272  pwfir  9279  pwfi  9281  fiint  9289  residfi  9298  unifpw  9315  wofib  9510  sucprcreg  9571  sucprcregOLD  9572  opthreg  9590  suc11reg  9591  infeq5  9609  rankwflemb  9768  r1elss  9781  pwwf  9782  unwf  9785  uniwf  9794  rankonid  9804  rankr1id  9837  rankuni  9838  rankxplim3  9856  scott0b  9869  scott0OLD  9870  karden  9891  kardenOLD  9892  djuexb  9907  isnum3  9952  oncard  9958  card1  9966  cardlim  9970  cardmin2  9997  pm54.43lem  9998  ween  10031  acnnum  10048  alephsuc2  10076  alephgeom  10078  iscard3  10089  dfac3  10117  dfac4  10118  dfac5lem3  10121  dfac5  10124  dfac2  10127  dfac8  10131  dfac9  10132  dfacacn  10137  dfac13  10138  dfac12r  10142  dfac12k  10143  kmlem2  10147  kmlem13  10158  djuinf  10184  ackbij2  10237  cflim2  10258  isfin4-2  10309  isfin4p1  10310  isf33lem  10361  compsscnv  10366  fin1a2lem6  10400  domtriom  10438  ac9  10478  ac9s  10488  fodomb  10521  brdom3  10523  brdom5  10524  brdom4  10525  brdom7disj  10526  brdom6disj  10527  iunfo  10534  sdomsdomcard  10555  gch2  10671  gch3  10672  eltsk2g  10747  grutsk  10818  ordpipq  10938  ltbtwnnq  10974  mappsrpr  11104  map2psrpr  11106  elreal2  11128  le2tri3i  11351  elnn0nn  12557  elnnnn0b  12559  elnnnn0c  12560  elnnz  12612  elnn0z  12615  elz2  12620  elnnz1  12631  0nn0m1nnn0  12662  eluz2b2  12957  elnn1uz2  12961  elpqb  13012  elioo4g  13445  eluzfz2b  13573  fzn0  13578  elfz1end  13595  fzass4  13603  elfz1b  13634  nn0fz0  13666  fzolb  13707  fzon0  13719  elfzo0  13742  elfzo0z  13743  elfzo1  13754  fzo1fzo0n0  13757  om2uzrani  14002  nn0opthi  14320  hashkf  14382  isfinite4  14412  hashprb  14447  hashf1  14508  elss2prb  14539  iswrdb  14571  wrdexb  14576  0wrd0  14591  wrdl3s3  15019  cotr2g  15033  trclun  15071  rexanuz  15417  rexuz3  15420  fsum0diag  15847  fprod0diag  16059  divalgmod  16482  sadcp1  16531  isprm6  16791  nnoddn2prmb  16891  4sqlem4  17030  fnpr2ob  17630  mreunirn  17671  isdrs2  18380  isacs5  18622  isacs4  18623  isacs3  18624  dfgrp2  19053  dfgrp3  19129  dfgrp3e  19130  isnsg3  19250  gicer  19371  oppgmndb  19449  oppggrpb  19452  pmtrfb  19559  invghm  19927  isringrng  20395  dfring2  20396  opprrngb  20454  opprringb  20456  ricer  20634  isnzr2hash  20647  isdomn4  20844  abvn0b  20969  gzrngunit  21613  dvdsrzring  21641  zringunit  21646  zlmlmod  21702  cygth  21751  frgpcyg  21753  zlmassa  22083  toprntopon  23112  tgclb  23157  iscldtop  23282  isnrm2  23545  isnrm3  23546  discmp  23585  dfconn2  23606  2ndcsb  23636  dis2ndc  23648  loclly  23675  unisngl  23715  locfindis  23718  iskgen2  23736  dfac14  23806  kqtop  23933  kqt0  23934  kqreg  23939  kqnrm  23940  hmpher  23972  hmphsymb  23974  hmph0  23983  kqhmph  24007  ist1-5lem  24008  elmptrab2  24016  isfil2  24044  filunirn  24070  isufil2  24096  hausflim  24169  isfcls  24197  alexsubALT  24239  istgp2  24279  ustbas  24415  xmetunirn  24525  dscmet  24760  dscopn  24761  isngp4  24800  zcld  25002  zlmclm  25302  iscmet2  25484  iundisj  25738  i1f1lem  25879  fta1b  26360  elply2  26384  elqaa  26514  aannenlem2  26523  wilth  27266  lgsne0  27530  2lgs  27602  2sqlem2  27613  ostth  27834  elno2  27849  bdayfo  27872  elons2  28482  eln0s2  28581  eln0s  28585  elzn0s  28622  eln0zs  28624  elnnzs  28625  remulscllem1  28724  mpteleeOLD  29276  wrdupgr  29466  wrdumgr  29478  umgrislfupgr  29504  lfuhgr3  29531  uspgrupgrushgr  29563  usgrumgruspgr  29566  usgruspgrb  29567  usgrislfuspgr  29571  uvtx01vtx  29781  pthspthcyc  30194  spthcycl  30195  wwlksnwwlksnon  30307  elwwlks2ons3  30347  clwwlkn1loopb  30437  eclclwwlkn1  30469  upgriseupth  30605  numclwwlkovh  30771  nmlno0lem  31192  isblo3i  31200  blocni  31204  hvsubeq0i  31462  hvaddcani  31464  bcseqi  31519  isch3  31640  norm1exi  31649  hhsssh  31668  shslubi  31784  dfch2  31806  pjoc1i  31830  pjchi  31831  shs00i  31849  chsscon3i  31860  chlejb1i  31875  chj00i  31886  shjshseli  31892  h1de2ctlem  31954  spanunsni  31978  cmcmi  31991  cmbr3i  31999  cmbr4i  32000  pj11i  32110  hosubeq0i  32225  dmadjrnb  32305  nmlnop0iALT  32394  lnopeq0i  32406  elunop2  32412  lnconi  32432  lncnopbd  32436  adjbdlnb  32483  adjbd1o  32484  adjeq0  32490  rnbra  32506  pjss1coi  32562  pjss2coi  32563  pjnormssi  32567  pjssdif2i  32573  pjssdif1i  32574  dfpjop  32581  pjinvari  32590  pjin2i  32592  pjci  32599  pjcmul1i  32600  pjcmul2i  32601  strb  32657  hstrbi  32665  mdsl1i  32720  atom1d  32752  chrelat2i  32764  cvbr4i  32766  cvexchi  32768  sumdmdi  32819  dmdbr4ati  32820  dmdbr5ati  32821  dmdbr6ati  32822  dmdbr7ati  32823  cdj3i  32840  eqtrb  32867  difeq  32911  iundisjf  32981  fpwrelmap  33124  iundisjfi  33187  xrge0tsmsbi  33434  dflring2  33823  dfufd2  33880  0mplrim  33944  ccfldextdgrr  34102  issgon  34553  measbasedom  34633  oddpwdc  34785  eulerpartlemt  34802  ballotlem2  34920  ballotlemrinv  34965  bnj1533  35281  bnj983  35380  r1omhf  35534  r1omhfb  35542  fineqvomonb  35565  fineqvnttrclse  35570  r1omhfbregs  35583  fineqvr1ombregs  35584  kardeq0  35602  karddom  35607  kardsdom  35608  kardexen  35609  satfv1  35868  satf0op  35882  fmla0xp  35888  fmla1  35892  elmsta  36053  antnestlaw1  36196  antnestlaw2  36197  antnestlaw3  36198  nepss  36223  dfon2  36295  distel  36306  fnimage  36432  altopthsn  36466  ellines  36657  rankeq1o  36676  opnrebl2  36865  df3nandALT1  36943  ttc00  37052  ttcwf  37068  ttcwf2  37069  ttcexbi  37077  ttc0el  37079  bj-animbi  37184  bj-dfbi6  37201  bj-consensus  37204  bj-falor2  37211  bj-bibibi  37212  bj-andnotim  37214  bj-alextruim  37292  bj-exextruan  37293  bj-ssbeq  37308  bj-19.41al  37314  bj-subst  37316  bj-eqs  37331  bj-cbvexw  37332  bj-sb  37345  bj-substax12  37382  bj-dfnnf3  37439  bj-equs45fv  37479  bj-hbaeb2  37486  bj-hbnaeb  37488  bj-equsal  37494  bj-sbsb  37505  bj-moeub  37517  bj-csbsnlem  37571  bj-snsetex  37632  bj-snglex  37642  bj-1uplth  37676  bj-1uplex  37677  bj-2uplth  37690  bj-2uplex  37691  bj-bm1.3ii  37733  bj-restpw  37767  bj-restuni  37772  bj-discrmoore  37786  bj-snmooreb  37789  bj-elid6  37847  bj-eldiag2  37854  mptsnunlem  38017  topdifinf  38028  elxp8  38050  finxp1o  38071  wl-moae  38204  wl-exeq  38222  wl-aleq  38223  wl-nfeqfb  38224  volsupnfl  38349  cover2  38399  isbnd3  38468  cntotbnd  38480  heibor  38505  isfld2  38689  isfldidl  38752  orfa  38766  eqbrb  38921  eqelb  38923  iss2  39026  issetssr  39265  n0el3  39418  detlem  39568  petlem  39597  eldisjs6  39622  prtlem16  39676  isltrn2N  40927  aks6d1c2p2  42919  aks6d1c6isolem3  42976  sn-iotalem  43025  dffltz  43399  eu6w  43441  3cubes  43454  ismrc  43465  isnacs3  43474  rexzrexnn0  43564  eldioph4b  43571  dford3  43788  wopprc  43790  ttac  43796  pw2f1ocnv  43797  dfac11  43822  dfac21  43826  isnumbasabl  43866  isnumbasgrp  43867  dfacbasgrp  43868  aaitgo  43922  dflim5  44089  nvocnvb  44181  dfno2  44187  ifpbi1b  44262  rp-fakeimass  44271  rp-fakeanorass  44272  rp-isfinite5  44276  rp-isfinite6  44277  dfsucon  44282  snen1g  44283  iscard4  44292  rtrclex  44376  cnvtrrel  44429  frege54cor0a  44622  isotone1  44807  isotone2  44808  gneispace  44893  k0004lem3  44908  grumnueq  45030  ismnushort  45044  nanorxor  45048  nzss  45060  pm10.55  45112  pm11.57  45132  pm13.192  45153  pm13.194  45155  ipo0  45191  ifr0  45192  xpexb  45195  3impexpbicom  45222  com3rgbi  45256  pm2.43bgbi  45259  pm2.43cbi  45260  sb5ALT  45267  trsbc  45282  2pm13.193  45294  ax6e2ndeq  45301  2uasbanh  45303  eelT01  45452  eel0T1  45453  uunT1  45521  zfregs2VD  45582  equncomVD  45609  trsbcVD  45618  undif3VD  45623  2pm13.193VD  45644  ax6e2eqVD  45648  ax6e2ndeqVD  45650  2uasbanhVD  45652  ax6e2ndeqALT  45672  tcfr  45705  mptssid  45989  elfzfzo  46029  allbutfi  46141  uzn0bi  46206  dvnprodlem3  46695  elaa2  46981  sge00  47123  elhoi  47289  ovn0  47313  ovolval4lem2  47397  confun  47709  afvfv0bi  47922  ffnafv  47941  afv2ndefb  47994  dfatafv2rnb  47997  afv2fv0b  48036  prpair  48283  sbcpr  48303  fpprel2  48539  sbgoldbmb  48584  vopnbgrelself  48653  isgrtri  48741  stgr1  48759  mgm2mgm  49025  nnpw2pb  49400  0aryfvalel  49447  mo0sn  49627  resinsnlem  49682  homf0  49820  isoval2  49846  oppccicb  49862  oppcciceq  49863  funcf2lem2  49893  initc  49902  isinito2  50310  isinito3  50311  termc  50330  dftermc3  50342  elsetrecs  50511  elpg  50525