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  2196  19.3  2239  19.41  2272  sbalex  2279  equsexv  2303  sbim  2337  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  3121  r19.26  3123  r19.21v  3188  gencbvex  3507  gencbvex2  3508  pm13.183  3620  rr19.3v  3621  rr19.28v  3622  euxfr2w  3678  euxfr2  3680  reu6  3684  reu3  3685  reuan  3844  dfss2  3917  sspss  4050  complss  4098  unineq  4234  uneqin  4235  difrab  4264  un00  4357  vvin  4359  sbnfc2  4397  ssdifeq0  4442  r19.2zb  4456  ralidmw  4472  ralidm  4473  pwidb  4579  snidb  4622  rabsnifsb  4683  tppreqb  4768  difsnb  4769  pwpw0  4774  sssn  4787  preq12b  4810  unissint  4932  uniintsn  4945  iununi  5059  al0ssb  5262  intex  5305  intnex  5306  axpweq  5312  iin0  5324  nfcvb  5338  eusvnfb  5355  eusv2nf  5357  ralxfrALT  5377  sspwb  5417  unipw  5418  opnz  5442  opth  5445  sbcop1  5458  opeqsng  5475  propeqop  5479  opthwiener  5487  opthhausdorff  5490  opthhausdorff0  5491  rexopabb  5502  ssopab2bw  5522  ssopab2b  5524  pwssun  5543  opelxp  5687  opthprc  5715  relsnb  5780  relop  5828  issetid  5832  xpid11  5914  elinxp  6008  eldmeldmressn  6014  iss  6027  iresn0n0  6046  asymref2  6111  xpnz  6150  xpdifid  6159  xpdifcnvepel  6160  ssrnres  6170  dfrel2  6181  relcnvtrg  6267  resssxp  6271  relrelss  6274  unixp0  6285  reuop  6295  dfpo2  6298  fn0  6668  funssxp  6736  f00  6762  f0bi  6763  dffo2  6798  f1o00  6858  fo00  6859  fv3  6901  dffn5  6941  dff2  7097  dff3  7098  dffo4  7101  dffo5  7102  exfo  7103  fmpt  7108  fompt  7116  ffnfv  7117  fsn  7134  fsn2  7135  funop  7151  funsneqopb  7154  fnsnbOLD  7169  isores1  7340  ssoprab2b  7487  eqoprab2bw  7488  eqfnov2  7548  unexb  7761  uniexb  7776  pwexb  7778  iunpw  7783  ordeleqon  7794  dford5  7796  onintrab  7808  ordsuc  7823  unon  7840  onuninsuci  7849  ordzsl  7854  onzsl  7855  f1oexbi  7938  ffoss  7956  1st2ndb  8039  frxp3  8161  suppssov1  8207  suppssov2  8208  suppssfv  8212  reldmtpos  8244  dfrecs3  8373  omopthi  8663  brinxper  8740  ecopover  8835  fsetexb  8879  mapsncnv  8914  mptelixpg  8956  elixpsn  8958  ixpsnf1o  8959  bren2  9003  en0  9038  en0ALT  9039  en0r  9040  en1  9044  en1b  9045  sbthb  9110  dom0  9117  canth2  9142  onfin2  9225  sdom1  9234  1sdom2dom  9238  fineqv  9251  unfilem1  9290  unfib  9294  pwfir  9301  pwfi  9303  fiint  9311  residfi  9320  unifpw  9337  wofib  9532  sucprcreg  9593  sucprcregOLD  9594  opthreg  9612  suc11reg  9613  infeq5  9631  rankwflemb  9793  rankwflembOLD  9794  r1elss  9807  pwwf  9808  unwf  9811  uniwf  9821  rankonid  9832  rankr1id  9871  rankuni  9872  rankxplim3  9891  elhf4  9905  elhf3OLD  9916  scott0b  9930  scott0OLD  9931  karden  9952  kardenOLD  9953  djuexb  9983  isnum3  10028  oncard  10034  card1  10042  cardlim  10046  cardmin2  10073  pm54.43lem  10074  ween  10107  acnnum  10124  alephsuc2  10152  alephgeom  10154  iscard3  10165  dfac3  10193  dfac4  10194  dfac5lem3  10197  dfac5  10200  dfac2  10203  dfac8  10207  dfac9  10208  dfacacn  10213  dfac13  10214  dfac12r  10218  dfac12k  10219  kmlem2  10223  kmlem13  10234  djuinf  10260  ackbij2  10313  cflim2  10334  isfin4-2  10385  isfin4p1  10386  isf33lem  10437  compsscnv  10442  fin1a2lem6  10476  domtriom  10514  ac9  10554  ac9s  10564  fodomb  10598  brdom3  10600  brdom5  10601  brdom4  10602  brdom7disj  10603  brdom6disj  10604  iunfo  10616  sdomsdomcard  10637  gch2  10753  gch3  10754  eltsk2g  10829  grutsk  10900  ordpipq  11020  ltbtwnnq  11056  mappsrpr  11186  map2psrpr  11188  elreal2  11210  le2tri3i  11433  elnn0nn  12641  elnnnn0b  12643  elnnnn0c  12644  elnnz  12696  elnn0z  12699  elz2  12704  elnnz1  12715  0nn0m1nnn0  12746  eluz2b2  13041  elnn1uz2  13045  elpqb  13097  elioo4g  13530  eluzfz2b  13659  fzn0  13664  elfz1end  13681  fzass4  13689  elfz1b  13720  nn0fz0  13752  fzolb  13793  fzon0  13805  elfzo0  13828  elfzo0z  13829  elfzo1  13840  fzo1fzo0n0  13843  om2uzrani  14088  nn0opthi  14407  hashkf  14469  isfinite4  14499  hashprb  14534  hashf1  14595  elss2prb  14626  iswrdb  14658  wrdexb  14663  0wrd0  14678  s3rex  15094  wrdl3s3  15108  cotr2g  15122  trclun  15160  rexanuz  15506  rexuz3  15509  fsum0diag  15936  fprod0diag  16146  divalgmod  16569  sadcp1  16618  isprm6  16883  nnoddn2prmb  16984  4sqlem4  17123  fnpr2ob  17723  mreunirn  17764  isdrs2  18473  isacs5  18715  isacs4  18716  isacs3  18717  dfgrp2  19166  dfgrp3  19242  dfgrp3e  19243  isnsg3  19363  gicer  19484  oppgmndb  19562  oppggrpb  19565  pmtrfb  19672  invghm  20040  isringrng  20509  dfring2  20510  opprrngb  20569  opprringb  20571  ricer  20749  isnzr2hash  20763  isdomn4  20960  isdrng2  20990  abvn0b  21086  gzrngunit  21732  dvdsrzring  21760  zringunit  21765  zlmlmod  21821  cygth  21870  frgpcyg  21872  zlmassa  22204  toprntopon  23236  tgclb  23281  iscldtop  23406  isnrm2  23669  isnrm3  23670  discmp  23709  dfconn2  23730  2ndcsb  23760  dis2ndc  23772  loclly  23799  unisngl  23839  locfindis  23842  iskgen2  23860  dfac14  23930  kqtop  24057  kqt0  24058  kqreg  24063  kqnrm  24064  hmpher  24096  hmphsymb  24098  hmph0  24107  kqhmph  24131  ist1-5lem  24132  elmptrab2  24140  isfil2  24168  filunirn  24194  isufil2  24220  hausflim  24293  isfcls  24321  alexsubALT  24363  istgp2  24403  ustbas  24539  xmetunirn  24649  dscmet  24884  dscopn  24885  isngp4  24924  zcld  25126  zlmclm  25426  iscmet2  25608  iundisj  25862  i1f1lem  26003  fta1b  26483  elply2  26507  elqaa  26638  aannenlem2  26649  wilth  27391  lgsne0  27655  2lgs  27727  2sqlem2  27738  ostth  27959  elno2  28004  bdayfo  28027  elons2  28637  eln0s2  28736  eln0s  28740  elzn0s  28777  eln0zs  28779  elnnzs  28780  remulscllem1  28879  mpteleeOLD  29466  wrdupgr  29656  wrdumgr  29668  umgrislfupgr  29694  lfuhgr3  29721  uspgrupgrushgr  29753  usgrumgruspgr  29756  usgruspgrb  29757  usgrislfuspgr  29761  uvtx01vtx  29971  pthspthcyc  30384  spthcycl  30385  wwlksnwwlksnon  30497  elwwlks2ons3  30537  clwwlkn1loopb  30627  eclclwwlkn1  30659  upgriseupth  30801  numclwwlkovh  30967  nmlno0lem  31388  isblo3i  31396  blocni  31400  hvsubeq0i  31658  hvaddcani  31660  bcseqi  31715  isch3  31836  norm1exi  31845  hhsssh  31864  shslubi  31980  dfch2  32002  pjoc1i  32026  pjchi  32027  shs00i  32045  chsscon3i  32056  chlejb1i  32071  chj00i  32082  shjshseli  32088  h1de2ctlem  32150  spanunsni  32174  cmcmi  32187  cmbr3i  32195  cmbr4i  32196  pj11i  32306  hosubeq0i  32421  dmadjrnb  32501  nmlnop0iALT  32590  lnopeq0i  32602  elunop2  32608  lnconi  32628  lncnopbd  32632  adjbdlnb  32679  adjbd1o  32680  adjeq0  32686  rnbra  32702  pjss1coi  32758  pjss2coi  32759  pjnormssi  32763  pjssdif2i  32769  pjssdif1i  32770  dfpjop  32777  pjinvari  32786  pjin2i  32788  pjci  32795  pjcmul1i  32796  pjcmul2i  32797  strb  32853  hstrbi  32861  mdsl1i  32916  atom1d  32948  chrelat2i  32960  cvbr4i  32962  cvexchi  32964  sumdmdi  33015  dmdbr4ati  33016  dmdbr5ati  33017  dmdbr6ati  33018  dmdbr7ati  33019  cdj3i  33036  eqtrb  33063  difeq  33107  iundisjf  33176  fpwrelmap  33318  iundisjfi  33381  xrge0tsmsbi  33628  dflring2  34018  dfufd2  34075  0mplrim  34139  ccfldextdgrr  34297  issgon  34748  measbasedom  34828  oddpwdc  34979  eulerpartlemt  34996  ballotlem2  35114  ballotlemrinv  35159  bnj1533  35475  bnj983  35574  r1omhfb  35727  fineqvomonb  35770  fineqvnttrclse  35775  r1omhfbregs  35788  fineqvr1ombregs  35789  kardeq0  35807  karddom  35812  kardsdom  35813  kardexen  35814  satfv1  36107  satf0op  36121  fmla0xp  36127  fmla1  36131  elmsta  36292  antnestlaw1  36435  antnestlaw2  36436  antnestlaw3  36437  nepss  36462  dfon2  36534  distel  36545  fnimage  36671  altopthsn  36706  ellines  36897  rankeq1o  36912  opnrebl2  37089  df3nandALT1  37167  ttc00  37276  ttcwf  37292  ttcwf2  37293  ttcexbi  37301  ttc0el  37303  bj-animbi  37408  bj-dfbi6  37425  bj-consensus  37428  bj-falor2  37435  bj-bibibi  37436  bj-andnotim  37438  bj-alextruim  37516  bj-exextruan  37517  bj-ssbeq  37532  bj-19.41al  37538  bj-subst  37540  bj-eqs  37555  bj-cbvexw  37556  bj-sb  37569  bj-substax12  37606  bj-dfnnf3  37663  bj-equs45fv  37703  bj-hbaeb2  37710  bj-hbnaeb  37712  bj-equsal  37718  bj-sbsb  37729  bj-moeub  37741  bj-csbsnlem  37795  bj-snsetex  37856  bj-snglex  37866  bj-1uplth  37900  bj-1uplex  37901  bj-2uplth  37914  bj-2uplex  37915  bj-bm1.3ii  37959  bj-restpw  37993  bj-restuni  37998  bj-discrmoore  38012  bj-snmooreb  38015  bj-elid6  38071  bj-eldiag2  38078  mptsnunlem  38241  topdifinf  38252  elxp8  38274  finxp1o  38295  wl-moae  38428  wl-exeq  38446  wl-aleq  38447  wl-nfeqfb  38448  volsupnfl  38563  cover2  38629  isbnd3  38698  cntotbnd  38710  heibor  38735  isfld2  38919  isfldidl  38982  orfa  38996  eqbrb  39151  eqelb  39153  iss2  39256  issetssr  39495  n0el3  39648  detlem  39798  petlem  39827  eldisjs6  39852  prtlem16  39906  isltrn2N  41157  aks6d1c2p2  43149  aks6d1c6isolem3  43206  sn-iotalem  43255  dffltz  43650  eu6w  43667  3cubes  43680  ismrc  43691  isnacs3  43700  rexzrexnn0  43790  eldioph4b  43797  dford3  44014  wopprc  44016  ttac  44022  pw2f1ocnv  44023  dfac11  44048  dfac21  44052  isnumbasabl  44092  isnumbasgrp  44093  dfacbasgrp  44094  aaitgo  44148  dflim5  44315  nvocnvb  44407  dfno2  44413  ifpbi1b  44488  rp-fakeimass  44497  rp-fakeanorass  44498  rp-isfinite5  44502  rp-isfinite6  44503  dfsucon  44508  snen1g  44509  iscard4  44518  rtrclex  44602  cnvtrrel  44655  frege54cor0a  44848  isotone1  45033  isotone2  45034  gneispace  45119  k0004lem3  45134  grumnueq  45256  ismnushort  45270  nanorxor  45274  nzss  45286  pm10.55  45338  pm11.57  45358  pm13.192  45379  pm13.194  45381  ipo0  45417  ifr0  45418  xpexb  45421  3impexpbicom  45448  com3rgbi  45482  pm2.43bgbi  45485  pm2.43cbi  45486  sb5ALT  45493  trsbc  45508  2pm13.193  45520  ax6e2ndeq  45527  2uasbanh  45529  eelT01  45678  eel0T1  45679  uunT1  45747  zfregs2VD  45808  equncomVD  45835  trsbcVD  45844  undif3VD  45849  2pm13.193VD  45870  ax6e2eqVD  45874  ax6e2ndeqVD  45876  2uasbanhVD  45878  ax6e2ndeqALT  45898  tcfr  45931  mptssid  46222  elfzfzo  46262  allbutfi  46373  uzn0bi  46438  dvnprodlem3  46927  elaa2  47213  sge00  47355  elhoi  47521  ovn0  47545  ovolval4lem2  47629  wrddin2  47867  chndin2  47872  chnrin2  47877  confun  47978  afvfv0bi  48191  ffnafv  48210  afv2ndefb  48263  dfatafv2rnb  48266  afv2fv0b  48305  prpair  48552  sbcpr  48572  fpprel2  48808  sbgoldbmb  48853  vopnbgrelself  48922  isgrtri  49010  stgr1  49028  mgm2mgm  49293  nnpw2pb  49668  0aryfvalel  49715  mo0sn  49895  resinsnlem  49948  homf0  50086  isoval2  50112  oppccicb  50128  oppcciceq  50129  funcf2lem2  50159  initc  50168  isinito2  50576  isinito3  50577  termc  50596  dftermc3  50608  elsetrecs  50762  elpg  50776