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  sbalexOLD  2282  equsexv  2307  sbim  2341  cbvalv1  2376  cbval  2433  equsex  2453  aecom  2462  equs45f  2494  dfsb1  2516  dfsb2  2528  sb6f  2532  dfmoeu  2566  moabs  2574  mo3  2595  mo4  2597  exmoeu  2612  moanimlem  2649  euan  2652  euanv  2655  2mo  2679  2eu6  2687  euae  2690  axextb  2741  eqcom  2773  nebi  3041  r19.35  3126  r19.26  3128  r19.21v  3193  gencbvex  3514  gencbvex2  3515  pm13.183  3628  rr19.3v  3629  rr19.28v  3630  euxfr2w  3686  euxfr2  3688  reu6  3692  reu3  3693  reuan  3853  dfss2  3926  sspss  4059  complss  4108  unineq  4244  uneqin  4245  difrab  4274  un00  4367  vvin  4369  sbnfc2  4407  ssdifeq0  4452  r19.2zb  4466  ralidmw  4482  ralidm  4483  pwidb  4589  snidb  4632  rabsnifsb  4693  tppreqb  4778  difsnb  4779  pwpw0  4784  sssn  4797  preq12b  4820  unissint  4942  uniintsn  4955  iununi  5070  al0ssb  5276  intex  5319  intnex  5320  axpweq  5326  iin0  5338  nfcvb  5352  eusvnfb  5369  eusv2nf  5371  ralxfrALT  5391  sspwb  5435  unipw  5436  opnz  5460  opth  5463  sbcop1  5475  opeqsng  5491  propeqop  5495  opthwiener  5502  opthhausdorff  5505  opthhausdorff0  5506  rexopabb  5517  ssopab2bw  5537  ssopab2b  5539  pwssun  5558  opelxp  5702  opthprc  5730  relsnb  5794  relop  5841  issetid  5845  xpid11  5927  elinxp  6023  eldmeldmressn  6029  iss  6042  iresn0n0  6061  asymref2  6122  xpnz  6161  xpdifid  6170  xpdifcnvepel  6171  ssrnres  6181  dfrel2  6192  relcnvtrg  6273  resssxp  6277  relrelss  6280  unixp0  6291  reuop  6301  dfpo2  6304  fn0  6673  funssxp  6741  f00  6767  f0bi  6768  dffo2  6803  f1o00  6863  fo00  6864  fv3  6906  dffn5  6946  dff2  7101  dff3  7102  dffo4  7105  dffo5  7106  exfo  7107  fmpt  7112  fompt  7120  ffnfv  7121  fsn  7138  fsn2  7139  funop  7153  funsneqopb  7156  fnsnbOLD  7171  isores1  7343  ssoprab2b  7492  eqoprab2bw  7493  eqfnov2  7553  unexb  7757  uniexb  7772  pwexb  7774  iunpw  7779  ordeleqon  7790  dford5  7792  onintrab  7804  ordsuc  7819  unon  7836  onuninsuci  7845  ordzsl  7850  onzsl  7851  f1oexbi  7934  ffoss  7952  1st2ndb  8035  frxp3  8156  suppssov1  8202  suppssov2  8203  suppssfv  8207  reldmtpos  8239  dfrecs3  8368  omopthi  8656  brinxper  8733  ecopover  8828  fsetexb  8870  mapsncnv  8900  mptelixpg  8942  elixpsn  8944  ixpsnf1o  8945  bren2  8989  en0  9024  en0ALT  9025  en0r  9026  en1  9030  en1b  9031  sbthb  9096  dom0  9103  canth2  9128  onfin2  9211  sdom1  9220  1sdom2dom  9224  fineqv  9237  unfilem1  9275  unfib  9279  pwfir  9286  pwfi  9288  fiint  9296  residfi  9305  unifpw  9322  wofib  9517  sucprcreg  9578  sucprcregOLD  9579  opthreg  9597  suc11reg  9598  infeq5  9616  rankwflemb  9775  r1elss  9788  pwwf  9789  unwf  9792  uniwf  9801  rankonid  9811  rankr1id  9844  rankuni  9845  rankxplim3  9863  scott0b  9876  scott0OLD  9877  karden  9898  kardenOLD  9899  djuexb  9914  isnum3  9959  oncard  9965  card1  9973  cardlim  9977  cardmin2  10004  pm54.43lem  10005  ween  10038  acnnum  10055  alephsuc2  10083  alephgeom  10085  iscard3  10096  dfac3  10124  dfac4  10125  dfac5lem3  10128  dfac5  10131  dfac2  10134  dfac8  10138  dfac9  10139  dfacacn  10144  dfac13  10145  dfac12r  10149  dfac12k  10150  kmlem2  10154  kmlem13  10165  djuinf  10191  ackbij2  10244  cflim2  10265  isfin4-2  10316  isfin4p1  10317  isf33lem  10368  compsscnv  10373  fin1a2lem6  10407  domtriom  10445  ac9  10485  ac9s  10495  fodomb  10528  brdom3  10530  brdom5  10531  brdom4  10532  brdom7disj  10533  brdom6disj  10534  iunfo  10541  sdomsdomcard  10562  gch2  10678  gch3  10679  eltsk2g  10754  grutsk  10825  ordpipq  10945  ltbtwnnq  10981  mappsrpr  11111  map2psrpr  11113  elreal2  11135  le2tri3i  11358  elnn0nn  12564  elnnnn0b  12566  elnnnn0c  12567  elnnz  12619  elnn0z  12622  elz2  12627  elnnz1  12638  eluz2b2  12963  elnn1uz2  12967  elpqb  13018  elioo4g  13451  eluzfz2b  13579  fzn0  13584  elfz1end  13601  fzass4  13609  elfz1b  13640  nn0fz0  13672  fzolb  13713  fzon0  13725  elfzo0  13748  elfzo0z  13749  elfzo1  13760  fzo1fzo0n0  13763  om2uzrani  14008  nn0opthi  14326  hashkf  14388  isfinite4  14418  hashprb  14453  hashf1  14514  elss2prb  14545  iswrdb  14577  wrdexb  14582  0wrd0  14597  wrdl3s3  15025  cotr2g  15039  trclun  15077  rexanuz  15423  rexuz3  15426  fsum0diag  15854  fprod0diag  16066  divalgmod  16489  sadcp1  16538  isprm6  16798  nnoddn2prmb  16898  4sqlem4  17037  fnpr2ob  17637  mreunirn  17678  isdrs2  18387  isacs5  18629  isacs4  18630  isacs3  18631  dfgrp2  19060  dfgrp3  19136  dfgrp3e  19137  isnsg3  19257  gicer  19378  oppgmndb  19456  oppggrpb  19459  pmtrfb  19566  invghm  19934  isringrng  20402  dfring2  20403  opprrngb  20461  opprringb  20463  ricer  20641  isnzr2hash  20654  isdomn4  20851  abvn0b  20976  gzrngunit  21620  dvdsrzring  21648  zringunit  21653  zlmlmod  21709  cygth  21758  frgpcyg  21760  zlmassa  22090  toprntopon  23119  tgclb  23164  iscldtop  23289  isnrm2  23552  isnrm3  23553  discmp  23592  dfconn2  23613  2ndcsb  23643  dis2ndc  23654  loclly  23681  unisngl  23721  locfindis  23724  iskgen2  23742  dfac14  23812  kqtop  23939  kqt0  23940  kqreg  23945  kqnrm  23946  hmpher  23978  hmphsymb  23980  hmph0  23989  kqhmph  24013  ist1-5lem  24014  elmptrab2  24022  isfil2  24050  filunirn  24076  isufil2  24102  hausflim  24175  isfcls  24203  alexsubALT  24245  istgp2  24285  ustbas  24421  xmetunirn  24531  dscmet  24766  dscopn  24767  isngp4  24806  zcld  25008  zlmclm  25308  iscmet2  25490  iundisj  25744  i1f1lem  25885  fta1b  26366  elply2  26390  elqaa  26520  aannenlem2  26529  wilth  27272  lgsne0  27536  2lgs  27608  2sqlem2  27619  ostth  27840  elno2  27855  bdayfo  27878  elons2  28488  eln0s2  28587  eln0s  28591  elzn0s  28628  eln0zs  28630  elnnzs  28631  remulscllem1  28730  mpteleeOLD  29282  wrdupgr  29472  wrdumgr  29484  umgrislfupgr  29510  uspgrupgrushgr  29566  usgrumgruspgr  29569  usgruspgrb  29570  usgrislfuspgr  29574  uvtx01vtx  29784  pthspthcyc  30189  wwlksnwwlksnon  30301  elwwlks2ons3  30341  clwwlkn1loopb  30431  eclclwwlkn1  30463  upgriseupth  30595  numclwwlkovh  30761  nmlno0lem  31182  isblo3i  31190  blocni  31194  hvsubeq0i  31452  hvaddcani  31454  bcseqi  31509  isch3  31630  norm1exi  31639  hhsssh  31658  shslubi  31774  dfch2  31796  pjoc1i  31820  pjchi  31821  shs00i  31839  chsscon3i  31850  chlejb1i  31865  chj00i  31876  shjshseli  31882  h1de2ctlem  31944  spanunsni  31968  cmcmi  31981  cmbr3i  31989  cmbr4i  31990  pj11i  32100  hosubeq0i  32215  dmadjrnb  32295  nmlnop0iALT  32384  lnopeq0i  32396  elunop2  32402  lnconi  32422  lncnopbd  32426  adjbdlnb  32473  adjbd1o  32474  adjeq0  32480  rnbra  32496  pjss1coi  32552  pjss2coi  32553  pjnormssi  32557  pjssdif2i  32563  pjssdif1i  32564  dfpjop  32571  pjinvari  32580  pjin2i  32582  pjci  32589  pjcmul1i  32590  pjcmul2i  32591  strb  32647  hstrbi  32655  mdsl1i  32710  atom1d  32742  chrelat2i  32754  cvbr4i  32756  cvexchi  32758  sumdmdi  32809  dmdbr4ati  32810  dmdbr5ati  32811  dmdbr6ati  32812  dmdbr7ati  32813  cdj3i  32830  eqtrb  32857  difeq  32901  iundisjf  32971  fpwrelmap  33115  iundisjfi  33178  xrge0tsmsbi  33425  dflring2  33814  dfufd2  33871  0mplrim  33935  ccfldextdgrr  34093  issgon  34544  measbasedom  34623  oddpwdc  34775  eulerpartlemt  34792  ballotlem2  34910  ballotlemrinv  34955  bnj1533  35271  bnj983  35370  r1omhf  35524  r1omhfb  35532  fineqvomonb  35555  fineqvnttrclse  35560  r1omhfbregs  35573  fineqvr1ombregs  35574  kardeq0  35592  karddom  35597  kardsdom  35598  kardexen  35599  0nn0m1nnn0  35627  lfuhgr3  35632  spthcycl  35641  satfv1  35875  satf0op  35889  fmla0xp  35895  fmla1  35899  elmsta  36060  antnestlaw1  36203  antnestlaw2  36204  antnestlaw3  36205  nepss  36230  dfon2  36302  distel  36313  fnimage  36439  altopthsn  36473  ellines  36664  rankeq1o  36683  opnrebl2  36872  df3nandALT1  36950  ttc00  37059  ttcwf  37075  ttcwf2  37076  ttcexbi  37084  ttc0el  37086  bj-animbi  37191  bj-dfbi6  37208  bj-consensus  37211  bj-falor2  37218  bj-bibibi  37219  bj-andnotim  37221  bj-alextruim  37299  bj-exextruan  37300  bj-ssbeq  37315  bj-19.41al  37321  bj-subst  37323  bj-eqs  37338  bj-cbvexw  37339  bj-sb  37352  bj-substax12  37389  bj-dfnnf3  37446  bj-equs45fv  37486  bj-hbaeb2  37493  bj-hbnaeb  37495  bj-equsal  37501  bj-sbsb  37512  bj-moeub  37524  bj-csbsnlem  37578  bj-snsetex  37639  bj-snglex  37649  bj-1uplth  37683  bj-1uplex  37684  bj-2uplth  37697  bj-2uplex  37698  bj-bm1.3ii  37740  bj-restpw  37774  bj-restuni  37779  bj-discrmoore  37793  bj-snmooreb  37796  bj-elid6  37854  bj-eldiag2  37861  mptsnunlem  38024  topdifinf  38035  elxp8  38057  finxp1o  38078  wl-moae  38211  wl-exeq  38229  wl-aleq  38230  wl-nfeqfb  38231  volsupnfl  38356  cover2  38406  isbnd3  38475  cntotbnd  38487  heibor  38512  isfld2  38696  isfldidl  38759  orfa  38773  eqbrb  38928  eqelb  38930  iss2  39033  issetssr  39272  n0el3  39425  detlem  39575  petlem  39604  eldisjs6  39629  prtlem16  39683  isltrn2N  40934  aks6d1c2p2  42926  aks6d1c6isolem3  42983  sn-iotalem  43032  dffltz  43406  eu6w  43448  3cubes  43461  ismrc  43472  isnacs3  43481  rexzrexnn0  43571  eldioph4b  43578  dford3  43795  wopprc  43797  ttac  43803  pw2f1ocnv  43804  dfac11  43829  dfac21  43833  isnumbasabl  43873  isnumbasgrp  43874  dfacbasgrp  43875  aaitgo  43929  dflim5  44096  nvocnvb  44188  dfno2  44194  ifpbi1b  44269  rp-fakeimass  44278  rp-fakeanorass  44279  rp-isfinite5  44283  rp-isfinite6  44284  dfsucon  44289  snen1g  44290  iscard4  44299  rtrclex  44383  cnvtrrel  44436  frege54cor0a  44629  isotone1  44814  isotone2  44815  gneispace  44900  k0004lem3  44915  grumnueq  45037  ismnushort  45051  nanorxor  45055  nzss  45067  pm10.55  45119  pm11.57  45139  pm13.192  45160  pm13.194  45162  ipo0  45198  ifr0  45199  xpexb  45202  3impexpbicom  45229  com3rgbi  45263  pm2.43bgbi  45266  pm2.43cbi  45267  sb5ALT  45274  trsbc  45289  2pm13.193  45301  ax6e2ndeq  45308  2uasbanh  45310  eelT01  45459  eel0T1  45460  uunT1  45528  zfregs2VD  45589  equncomVD  45616  trsbcVD  45625  undif3VD  45630  2pm13.193VD  45651  ax6e2eqVD  45655  ax6e2ndeqVD  45657  2uasbanhVD  45659  ax6e2ndeqALT  45679  tcfr  45712  mptssid  45996  elfzfzo  46036  allbutfi  46148  uzn0bi  46213  dvnprodlem3  46702  elaa2  46988  sge00  47130  elhoi  47296  ovn0  47320  ovolval4lem2  47404  confun  47716  afvfv0bi  47929  ffnafv  47948  afv2ndefb  48001  dfatafv2rnb  48004  afv2fv0b  48043  prpair  48290  sbcpr  48310  fpprel2  48546  sbgoldbmb  48591  vopnbgrelself  48660  isgrtri  48748  stgr1  48766  mgm2mgm  49032  nnpw2pb  49407  0aryfvalel  49454  mo0sn  49634  resinsnlem  49689  homf0  49827  isoval2  49853  oppccicb  49869  oppcciceq  49870  funcf2lem2  49900  initc  49909  isinito2  50317  isinito3  50318  termc  50337  dftermc3  50349  elsetrecs  50518  elpg  50532