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  1912  19.21v  1974  19.23v  1977  19.41v  1984  19.3v  2017  19.9v  2019  equcom  2053  cbvalw  2070  alcomw  2080  excomw  2081  exexw  2088  sbbii  2115  sban  2119  sbv  2127  sbrimvw  2130  alcom  2199  19.3  2242  19.41  2275  sbalex  2282  equsexv  2306  sbim  2340  cbvalv1  2374  cbval  2430  equsex  2450  aecom  2459  equs45f  2491  dfsb1  2513  dfsb2  2525  sb6f  2529  dfmoeu  2563  moabs  2571  mo3  2592  mo4  2594  exmoeu  2609  moanimlem  2646  euan  2649  euanv  2652  2mo  2676  2eu6  2684  euae  2687  axextb  2738  eqcom  2770  nebi  3039  r19.35  3124  r19.26  3126  r19.21v  3191  gencbvex  3510  gencbvex2  3511  pm13.183  3623  rr19.3v  3624  rr19.28v  3625  euxfr2w  3681  euxfr2  3683  reu6  3687  reu3  3688  reuan  3848  sspss  4032  complss  4090  dfss2  4097  unineq  4236  uneqin  4237  difrab  4266  un00  4360  vvin  4362  sbnfc2  4400  ssdifeq0  4445  r19.2zb  4459  ralidmw  4475  ralidm  4476  pwidb  4583  snidb  4623  rabsnifsb  4685  tppreqb  4770  difsnb  4771  sssn  4787  preq12b  4810  pwpw0  4836  unissint  4937  uniintsn  4950  iununi  5064  al0ssb  5268  intex  5312  intnex  5313  axpweq  5319  iin0  5331  nfcvb  5345  eusvnfb  5362  eusv2nf  5364  ralxfrALT  5384  sspwb  5424  unipw  5425  opnz  5449  opth  5452  sbcop1  5465  opeqsng  5482  propeqop  5486  opthwiener  5494  opthhausdorff  5497  opthhausdorff0  5498  rexopabb  5509  ssopab2bw  5529  ssopab2b  5531  pwssun  5550  opelxp  5694  opthprc  5722  relsnb  5789  relop  5838  issetid  5842  xpid11  5926  elinxp  6026  eldmeldmressn  6032  iss  6045  iresn0n0  6064  asymref2  6129  xpnz  6168  xpdifid  6177  xpdifcnvepel  6178  ssrnres  6188  dfrel2  6199  coass  6290  relcnvtrg  6292  resssxp  6296  relrelss  6299  unixp0  6310  reuop  6322  dfpo2  6325  fn0  6700  funssxp  6768  f00  6794  f0bi  6795  dffo2  6830  f1o00  6891  fo00  6892  fv3  6934  dffn5  6974  dff2  7131  dff3  7132  dffo4  7135  dffo5  7136  exfo  7137  fmpt  7142  fompt  7150  ffnfv  7151  fsn  7168  fsn2  7169  funop  7185  funsneqopb  7188  isores1  7373  ssoprab2b  7520  eqoprab2bw  7521  eqfnov2  7581  unexb  7795  uniexb  7810  pwexb  7812  iunpw  7817  ordeleqon  7830  dford5  7832  onintrab  7844  ordsuc  7859  unon  7876  onuninsuci  7885  ordzsl  7890  onzsl  7891  f1oexbi  7974  ffoss  7992  1st2ndb  8075  frxp3  8205  suppssov1  8252  suppssov2  8253  suppssfv  8257  reldmtpos  8289  dfrecs3  8418  omopthi  8708  brinxper  8785  ecopover  8880  fsetexb  8924  mapsncnv  8959  mptelixpg  9001  elixpsn  9003  ixpsnf1o  9004  bren2  9048  en0  9083  en0ALT  9084  en0r  9085  en1  9089  en1b  9090  sbthb  9155  dom0  9162  canth2  9187  onfin2  9270  sdom1  9279  1sdom2dom  9283  fineqv  9296  unfilem1  9335  unfib  9339  pwfir  9346  pwfi  9348  fiint  9356  residfi  9365  unifpw  9382  wofib  9576  sucprcreg  9637  sucprcregOLD  9638  opthreg  9656  suc11reg  9657  infeq5  9675  rankwflemb  9837  rankwflembOLD  9838  r1elss  9851  pwwf  9852  unwf  9855  uniwf  9865  rankonid  9876  rankr1id  9915  rankuni  9916  rankxplim3  9935  elhf4  9949  elhf3OLD  9960  scott0b  9974  scott0OLD  9975  karden  9996  kardenOLD  9997  djuexb  10027  isnum3  10072  oncard  10078  card1  10086  cardlim  10090  cardmin2  10119  pm54.43lem  10120  ween  10153  acnnum  10170  alephsuc2  10198  alephgeom  10200  iscard3  10211  dfac3  10239  dfac4  10240  dfac5lem3  10243  dfac5  10246  dfac2  10249  dfac8  10253  dfac9  10254  dfacacn  10259  dfac13  10260  dfac12r  10264  dfac12k  10265  kmlem2  10269  kmlem13  10280  djuinf  10306  ackbij2  10359  cflim2  10380  isfin4-2  10431  isfin4p1  10432  isf33lem  10483  compsscnv  10488  fin1a2lem6  10522  domtriom  10560  ac9  10600  ac9s  10610  fodomb  10644  brdom3  10646  brdom5  10647  brdom4  10648  brdom7disj  10649  brdom6disj  10650  iunfo  10662  sdomsdomcard  10683  gch2  10799  gch3  10800  eltsk2g  10875  grutsk  10946  ordpipq  11066  ltbtwnnq  11102  mappsrpr  11232  map2psrpr  11234  elreal2  11256  le2tri3i  11479  elnn0nn  12688  elnnnn0b  12690  elnnnn0c  12691  elnnz  12743  elnn0z  12746  elz2  12751  elnnz1  12762  0nn0m1nnn0  12793  eluz2b2  13088  elnn1uz2  13092  elpqb  13144  elioo4g  13577  eluzfz2b  13706  fzn0  13711  elfz1end  13728  fzass4  13736  elfz1b  13767  nn0fz0  13799  fzolb  13840  fzon0  13852  elfzo0  13875  elfzo0z  13876  elfzo1  13887  fzo1fzo0n0  13890  om2uzrani  14135  nn0opthi  14455  hashkf  14517  isfinite4  14547  hashprb  14582  hashf1  14643  elss2prb  14674  iswrdb  14706  wrdexb  14711  0wrd0  14726  s3rex  15144  wrdl3s3  15158  cotr2g  15172  trclun  15210  rexanuz  15557  rexuz3  15560  fsum0diag  15987  fprod0diag  16197  divalgmod  16620  sadcp1  16669  isprm6  16934  nnoddn2prmb  17035  4sqlem4  17174  fnpr2ob  17780  mreunirn  17821  isdrs2  18530  isacs5  18772  isacs4  18773  isacs3  18774  dfgrp2  19223  dfgrp3  19299  dfgrp3e  19300  isnsg3  19420  gicer  19542  oppgmndb  19620  oppggrpb  19623  pmtrfb  19730  invghm  20098  isringrng  20567  dfring2  20568  opprrngb  20627  opprringb  20629  ricer  20807  isnzr2hash  20821  isdomn4  21018  isdrng2  21048  abvn0b  21144  gzrngunit  21793  dvdsrzring  21822  zringunit  21827  zlmlmod  21883  cygth  21932  frgpcyg  21934  zlmassa  22266  toprntopon  23298  tgclb  23343  iscldtop  23468  isnrm2  23731  isnrm3  23732  discmp  23771  dfconn2  23792  2ndcsb  23822  dis2ndc  23834  loclly  23861  unisngl  23901  locfindis  23904  iskgen2  23922  dfac14  23992  kqtop  24119  kqt0  24120  kqreg  24125  kqnrm  24126  hmpher  24158  hmphsymb  24160  hmph0  24169  kqhmph  24193  ist1-5lem  24194  elmptrab2  24202  isfil2  24230  filunirn  24256  isufil2  24282  hausflim  24355  isfcls  24383  alexsubALT  24425  istgp2  24465  ustbas  24601  xmetunirn  24711  dscmet  24946  dscopn  24947  isngp4  24986  zcld  25188  zlmclm  25488  iscmet2  25670  iundisj  25924  i1f1lem  26065  fta1b  26545  elply2  26569  elqaa  26702  aannenlem2  26713  wilth  27455  lgsne0  27719  2lgs  27791  2sqlem2  27802  ostth  28023  elno2  28068  bdayfo  28091  elons2  28701  eln0s2  28800  eln0s  28804  elzn0s  28841  eln0zs  28843  elnnzs  28844  remulscllem1  28943  mpteleeOLD  29530  wrdupgr  29720  wrdumgr  29732  umgrislfupgr  29758  lfuhgr3  29785  uspgrupgrushgr  29817  usgrumgruspgr  29820  usgruspgrb  29821  usgrislfuspgr  29825  uvtx01vtx  30035  pthspthcyc  30448  spthcycl  30449  wwlksnwwlksnon  30561  elwwlks2ons3  30601  clwwlkn1loopb  30691  eclclwwlkn1  30723  upgriseupth  30865  numclwwlkovh  31031  nmlno0lem  31452  isblo3i  31460  blocni  31464  hvsubeq0i  31722  hvaddcani  31724  bcseqi  31779  isch3  31900  norm1exi  31909  hhsssh  31928  shslubi  32044  dfch2  32066  pjoc1i  32090  pjchi  32091  shs00i  32109  chsscon3i  32120  chlejb1i  32135  chj00i  32146  shjshseli  32152  h1de2ctlem  32214  spanunsni  32238  cmcmi  32251  cmbr3i  32259  cmbr4i  32260  pj11i  32370  hosubeq0i  32485  dmadjrnb  32565  nmlnop0iALT  32654  lnopeq0i  32666  elunop2  32672  lnconi  32692  lncnopbd  32696  adjbdlnb  32743  adjbd1o  32744  adjeq0  32750  rnbra  32766  pjss1coi  32822  pjss2coi  32823  pjnormssi  32827  pjssdif2i  32833  pjssdif1i  32834  dfpjop  32841  pjinvari  32850  pjin2i  32852  pjci  32859  pjcmul1i  32860  pjcmul2i  32861  strb  32917  hstrbi  32925  mdsl1i  32980  atom1d  33012  chrelat2i  33024  cvbr4i  33026  cvexchi  33028  sumdmdi  33079  dmdbr4ati  33080  dmdbr5ati  33081  dmdbr6ati  33082  dmdbr7ati  33083  cdj3i  33100  eqtrb  33169  difeq  33213  iundisjf  33281  fpwrelmap  33421  iundisjfi  33484  xrge0tsmsbi  33734  dflring2  34129  dfufd2  34186  0mplrim  34257  ccfldextdgrr  34415  issgon  34866  measbasedom  34946  oddpwdc  35097  eulerpartlemt  35114  ballotlem2  35232  ballotlemrinv  35277  bnj1533  35593  bnj983  35692  reu6f  35820  rmo6  35821  eqhf  35861  dfac15  35886  dfac16  35887  fineqvomonb  35928  fineqvnttrclse  35933  eqhfregs  35946  fineqvhfbregs  35947  kardeq0  35965  karddom  35970  kardsdom  35971  kardexen  35972  dfk12  36053  dfk22  36054  dfk32  36055  satfv1  36336  satf0op  36350  fmla0xp  36356  fmla1  36360  elmsta  36521  antnestlaw1  36664  antnestlaw2  36665  antnestlaw3  36666  elpssex  36672  elpssmo  36673  nepss  36698  dfon2  36769  distel  36780  fnimage  36906  altopthsn  36941  ellines  37132  rankeq1o  37147  opnrebl2  37324  df3nandALT1  37402  ttc00  37511  ttcwf  37527  ttcwf2  37528  ttcexbi  37536  ttc0el  37538  bj-animbi  37643  bj-dfbi6  37660  bj-consensus  37663  bj-falor2  37670  bj-bibibi  37671  bj-andnotim  37673  bj-alextruim  37751  bj-exextruan  37752  bj-ssbeq  37767  bj-19.41al  37773  bj-subst  37775  bj-eqs  37790  bj-cbvexw  37791  bj-sb  37804  bj-substax12  37841  bj-dfnnf3  37898  bj-equs45fv  37938  bj-hbaeb2  37945  bj-hbnaeb  37947  bj-equsal  37953  bj-sbsb  37964  bj-moeub  37976  bj-csbsnlem  38030  bj-snsetex  38091  bj-snglex  38101  bj-1uplth  38135  bj-1uplex  38136  bj-2uplth  38149  bj-2uplex  38150  relssdmrnb  38194  relssresb  38195  coineq0  38208  cossidcnvss2  38222  cossidcnvss  38223  nvo  38228  nvo3  38230  bj-bm1.3ii  38249  bj-restpw  38283  bj-restuni  38288  bj-discrmoore  38302  bj-snmooreb  38305  bj-elid6  38359  bj-eldiag2  38366  mptsnunlem  38529  topdifinf  38540  elxp8  38562  finxp1o  38583  wl-moae  38716  wl-exeq  38734  wl-aleq  38735  wl-nfeqfb  38736  volsupnfl  38851  cover2  38917  isbnd3  38984  cntotbnd  38996  heibor  39021  isfld2  39205  isfldidl  39268  orfa  39282  eqbrb  39437  eqelb  39439  iss2  39542  issetssr  39781  n0el3  39934  detlem  40084  petlem  40113  eldisjs6  40138  prtlem16  40192  isltrn2N  41443  aks6d1c2p2  43435  aks6d1c6isolem3  43492  sn-iotalem  43542  dffltz  43936  eu6w  43953  3cubes  43966  ismrc  43978  isnacs3  43987  rexzrexnn0  44077  eldioph4b  44084  dford3  44301  wopprc  44303  ttac  44309  pw2f1ocnv  44310  dfac11  44330  dfac21  44334  isnumbasabl  44373  isnumbasgrp  44374  dfacbasgrp  44375  aaitgo  44429  dflim5  44592  nvocnvb  44684  dfno2  44690  ifpbi1b  44765  rp-fakeimass  44774  rp-fakeanorass  44775  rp-isfinite5  44779  rp-isfinite6  44780  dfsucon  44785  snen1g  44786  iscard4  44795  rtrclex  44878  cnvtrrel  44931  frege54cor0a  45124  isotone1  45309  isotone2  45310  gneispace  45395  k0004lem3  45410  grumnueq  45532  ismnushort  45546  nanorxor  45550  nzss  45562  pm10.55  45614  pm11.57  45634  pm13.192  45655  pm13.194  45657  ipo0  45692  ifr0  45693  xpexb  45696  3impexpbicom  45723  com3rgbi  45757  pm2.43bgbi  45760  pm2.43cbi  45761  sb5ALT  45768  trsbc  45783  2pm13.193  45795  ax6e2ndeq  45802  2uasbanh  45804  eelT01  45953  eel0T1  45954  uunT1  46022  zfregs2VD  46083  equncomVD  46110  trsbcVD  46119  undif3VD  46124  2pm13.193VD  46145  ax6e2eqVD  46149  ax6e2ndeqVD  46151  2uasbanhVD  46153  ax6e2ndeqALT  46173  tcfr  46217  mptssid  46526  elfzfzo  46566  allbutfi  46677  uzn0bi  46742  dvnprodlem3  47231  elaa2  47517  sge00  47659  elhoi  47825  ovn0  47849  ovolval4lem2  47933  wrddin2  48171  chndin2  48176  chnrin2  48181  confun  48282  afvfv0bi  48495  ffnafv  48514  afv2ndefb  48567  dfatafv2rnb  48570  afv2fv0b  48609  prpair  48856  sbcpr  48876  fpprel2  49112  sbgoldbmb  49157  vopnbgrelself  49226  isgrtri  49314  stgr1  49332  mgm2mgm  49597  nnpw2pb  50030  0aryfvalel  50077  mo0sn  50258  resinsnlem  50315  elixpmpt  50335  homf0  50454  isoval2  50480  oppccicb  50496  oppcciceq  50497  funcf2lem2  50527  initc  50537  isinito2  50965  isinito3  50966  termc  50985  dftermc3  50997  elsetrecs  51199  elpg  51213