Theorem impbii 208

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bicom  221  biid  261  2th  264  pm5.74  270  bitri  275  notnotb  315  con34b  316  notbi  319  bibi2i  338  con1b  359  con2b  360  bi2.04  389  imdi  391  pm4.8  394  pm4.81  395  impexp  452  ancom  462  anass  470  jcab  519  impimprbi  828  orcom  869  dfor2  901  oridm  904  orbi2i  912  or12  920  biorfi  938  pm4.72  949  oibabs  951  jaob  961  pm4.44  996  pm4.79  1003  andi  1007  pm4.82  1023  cases2ALT  1048  consensus  1052  3impexp  1359  3jaob  1427  nanass  1509  tbw-bijust  1701  tbw-negdf  1702  19.26  1874  19.35  1881  19.21v  1943  19.23v  1946  19.41v  1954  19.3v  1986  19.9v  1988  equcom  2022  cbvalw  2039  alcomw  2048  exexw  2055  sbbii  2080  sban  2084  sbv  2092  alcom  2157  19.3  2196  19.41  2229  sbalex  2236  equsexv  2260  sbim  2300  cbvalv1  2338  cbval  2398  equsex  2418  aecom  2427  equs45f  2459  dfsb1  2481  dfsb2  2493  sb6f  2497  dfmoeu  2531  moabs  2538  mobii  2543  mo3  2559  mo4  2561  exmoeu  2576  moanimlem  2615  euan  2618  euanv  2621  2mo  2645  2eu6  2653  euae  2656  axextb  2707  eqcom  2740  nebi  3022  ralcom3OLD  3099  r19.35  3109  r19.35OLD  3110  r19.26  3112  r19.21v  3180  ceqsexOLD  3525  ceqsexvOLD  3527  gencbvex  3536  gencbvex2  3537  pm13.183  3656  rr19.3v  3657  rr19.28v  3658  euxfr2w  3716  euxfr2  3718  reu6  3722  reu3  3723  reuan  3890  sspss  4099  complss  4146  unineq  4277  uneqin  4278  difrab  4308  ab0w  4373  sbnfc2  4436  un00  4442  disj  4447  ssdifeq0  4486  r19.2zb  4495  ralidmw  4507  ralidm  4511  ralf0  4513  pwidb  4623  snidb  4663  rabsnifsb  4726  tppreqb  4808  difsnb  4809  pwpw0  4816  sssn  4829  preq12b  4851  pwsnOLD  4901  unissint  4976  uniintsn  4991  iununi  5102  al0ssb  5308  intex  5337  intnex  5338  axpweq  5348  iin0  5360  nfcvb  5374  eusvnfb  5391  eusv2nf  5393  ralxfrALT  5413  sspwb  5449  unipw  5450  opnz  5473  opth  5476  sbcop1  5488  opeqsng  5503  propeqop  5507  opthwiener  5514  opthhausdorff  5517  opthhausdorff0  5518  rexopabb  5528  ssopab2bw  5547  ssopab2b  5549  pwssun  5571  opelxp  5712  opthprc  5739  relsnb  5801  relop  5849  issetid  5853  xpid11  5930  elinxp  6018  eldmeldmressn  6024  iss  6034  iresn0n0  6052  asymref2  6116  xpnz  6156  xpdifid  6165  ssrnres  6175  dfrel2  6186  resssxp  6267  relrelss  6270  unixp0  6280  reuop  6290  dfpo2  6293  fn0  6679  funssxp  6744  f00  6771  f0bi  6772  dffo2  6807  f1o00  6866  fo00  6867  fv3  6907  dffn5  6948  dff2  7098  dff3  7099  dffo4  7102  dffo5  7103  exfo  7104  fmpt  7107  ffnfv  7115  fsn  7130  fsn2  7131  funop  7144  funsneqopb  7147  fnsnb  7161  isores1  7328  ssoprab2b  7475  eqoprab2bw  7476  eqfnov2  7536  unexb  7732  uniexb  7748  pwexb  7750  iunpw  7755  ordeleqon  7766  dford5  7768  onintrab  7781  ordsuc  7798  unon  7816  onuninsuci  7826  ordzsl  7831  onzsl  7832  f1oexbi  7916  ffoss  7929  1st2ndb  8012  frxp3  8134  suppssov1  8180  suppssfv  8184  reldmtpos  8216  dfrecs3  8369  dfrecs3OLD  8370  omopthi  8657  ecopover  8812  fsetexb  8855  mapsncnv  8884  mptelixpg  8926  elixpsn  8928  ixpsnf1o  8929  bren2  8976  en0  9010  en0OLD  9011  en0ALT  9012  en0r  9013  en1  9018  en1OLD  9019  en1b  9020  en1bOLD  9021  sbthb  9091  dom0  9099  canth2  9127  pwfir  9173  pwfi  9175  onfin2  9228  sdom1  9239  sdom1OLD  9240  1sdom2dom  9244  1sdomOLD  9246  fineqv  9260  unfilem1  9307  fiint  9321  residfi  9330  pwfiOLD  9344  unifpw  9352  wofib  9537  sucprcreg  9593  opthreg  9610  suc11reg  9611  infeq5  9629  rankwflemb  9785  r1elss  9798  pwwf  9799  unwf  9802  uniwf  9811  rankonid  9821  rankr1id  9854  rankuni  9855  rankxplim3  9873  scott0  9878  karden  9887  djuexb  9901  isnum3  9946  oncard  9952  card1  9960  cardlim  9964  cardmin2  9991  pm54.43lem  9992  ween  10027  acnnum  10044  alephsuc2  10072  alephgeom  10074  iscard3  10085  dfac3  10113  dfac4  10114  dfac5lem3  10117  dfac5  10120  dfac2  10123  dfac8  10127  dfac9  10128  dfacacn  10133  dfac13  10134  dfac12r  10138  dfac12k  10139  kmlem2  10143  kmlem13  10154  djuinf  10180  ackbij2  10235  cflim2  10255  isfin4-2  10306  isfin4p1  10307  isf33lem  10358  compsscnv  10363  fin1a2lem6  10397  domtriom  10435  ac9  10475  ac9s  10485  fodomb  10518  brdom3  10520  brdom5  10521  brdom4  10522  brdom7disj  10523  brdom6disj  10524  iunfo  10531  sdomsdomcard  10552  gch2  10667  gch3  10668  eltsk2g  10743  grutsk  10814  ordpipq  10934  ltbtwnnq  10970  mappsrpr  11100  map2psrpr  11102  elreal2  11124  le2tri3i  11341  elnn0nn  12511  elnnnn0b  12513  elnnnn0c  12514  elnnz  12565  elnn0z  12568  elz2  12573  elnnz1  12585  eluz2b2  12902  elnn1uz2  12906  elpqb  12957  elioo4g  13381  eluzfz2b  13507  fzn0  13512  elfz1end  13528  fzass4  13536  elfz1b  13567  nn0fz0  13596  fzolb  13635  fzon0  13647  elfzo0  13670  elfzo0z  13671  elfzo1  13679  fzo1fzo0n0  13680  om2uzrani  13914  nn0opthi  14227  hashkf  14289  isfinite4  14319  hashprb  14354  hashf1  14415  elss2prb  14445  iswrdb  14467  wrdexb  14472  0wrd0  14487  wrdl3s3  14910  cotr2g  14920  trclun  14958  rexanuz  15289  rexuz3  15292  fsum0diag  15720  fprod0diag  15927  divalgmod  16346  sadcp1  16393  isprm6  16648  nnoddn2prmb  16743  4sqlem4  16882  fnpr2ob  17501  mreunirn  17542  isdrs2  18256  isacs5  18498  isacs4  18499  isacs3  18500  dfgrp2  18844  dfgrp3  18919  dfgrp3e  18920  isnsg3  19035  gicer  19145  oppgmndb  19217  oppggrpb  19220  pmtrfb  19328  invghm  19696  opprringb  20155  isnzr2hash  20291  isdomn4  20911  abvn0b  20913  gzrngunit  21004  dvdsrzring  21023  zringunit  21028  zlmlmod  21068  cygth  21119  frgpcyg  21121  zlmassa  21448  toprntopon  22419  tgclb  22465  iscldtop  22591  isnrm2  22854  isnrm3  22855  discmp  22894  dfconn2  22915  2ndcsb  22945  dis2ndc  22956  loclly  22983  unisngl  23023  locfindis  23026  iskgen2  23044  dfac14  23114  kqtop  23241  kqt0  23242  kqreg  23247  kqnrm  23248  hmpher  23280  hmphsymb  23282  hmph0  23291  kqhmph  23315  ist1-5lem  23316  elmptrab2  23324  isfil2  23352  filunirn  23378  isufil2  23404  hausflim  23477  isfcls  23505  alexsubALT  23547  istgp2  23587  ustbas  23724  xmetunirn  23835  dscmet  24073  dscopn  24074  isngp4  24113  zcld  24321  zlmclm  24620  iscmet2  24803  iundisj  25057  i1f1lem  25198  fta1b  25679  elply2  25702  elqaa  25827  aannenlem2  25834  wilth  26565  lgsne0  26828  2lgs  26900  2sqlem2  26911  ostth  27132  elno2  27147  bdayfo  27170  mptelee  28143  wrdupgr  28335  wrdumgr  28347  umgrislfupgr  28373  uspgrupgrushgr  28427  usgrumgruspgr  28430  usgruspgrb  28431  usgrislfuspgr  28434  uvtx01vtx  28644  wwlksnwwlksnon  29159  elwwlks2ons3  29199  clwwlkn1loopb  29286  eclclwwlkn1  29318  upgriseupth  29450  numclwwlkovh  29616  nmlno0lem  30034  isblo3i  30042  blocni  30046  hvsubeq0i  30304  hvaddcani  30306  bcseqi  30361  isch3  30482  norm1exi  30491  hhsssh  30510  shslubi  30626  dfch2  30648  pjoc1i  30672  pjchi  30673  shs00i  30691  chsscon3i  30702  chlejb1i  30717  chj00i  30728  shjshseli  30734  h1de2ctlem  30796  spanunsni  30820  cmcmi  30833  cmbr3i  30841  cmbr4i  30842  pj11i  30952  hosubeq0i  31067  dmadjrnb  31147  nmlnop0iALT  31236  lnopeq0i  31248  elunop2  31254  lnconi  31274  lncnopbd  31278  adjbdlnb  31325  adjbd1o  31326  adjeq0  31332  rnbra  31348  pjss1coi  31404  pjss2coi  31405  pjnormssi  31409  pjssdif2i  31415  pjssdif1i  31416  dfpjop  31423  pjinvari  31432  pjin2i  31434  pjci  31441  pjcmul1i  31442  pjcmul2i  31443  strb  31499  hstrbi  31507  mdsl1i  31562  atom1d  31594  chrelat2i  31606  cvbr4i  31608  cvexchi  31610  sumdmdi  31661  dmdbr4ati  31662  dmdbr5ati  31663  dmdbr6ati  31664  dmdbr7ati  31665  cdj3i  31682  eqtrb  31702  difeq  31744  iundisjf  31808  cnvoprabOLD  31933  fpwrelmap  31946  iundisjfi  31995  xrge0tsmsbi  32198  ccfldextdgrr  32735  issgon  33110  measbasedom  33189  oddpwdc  33342  eulerpartlemt  33359  ballotlem2  33476  ballotlemrinv  33521  bnj1533  33852  bnj983  33951  0nn0m1nnn0  34091  lfuhgr3  34099  spthcycl  34109  satfv1  34343  satf0op  34357  fmla0xp  34363  fmla1  34367  elmsta  34528  nepss  34676  dfon2  34753  distel  34764  fnimage  34890  altopthsn  34922  ellines  35113  rankeq1o  35132  opnrebl2  35195  df3nandALT1  35273  bj-animbi  35424  bj-dfbi6  35441  bj-consensus  35444  bj-falor2  35452  bj-bibibi  35453  bj-andnotim  35455  bj-cbval  35515  bj-cbvex  35516  bj-ssbeq  35519  bj-19.41al  35525  bj-subst  35527  bj-eqs  35541  bj-cbvexw  35542  bj-sb  35554  bj-substax12  35588  bj-dfnnf3  35624  bj-equs45fv  35678  bj-hbaeb2  35685  bj-hbnaeb  35687  bj-equsal  35693  bj-sbsb  35704  bj-moeub  35717  bj-csbsnlem  35772  bj-snsetex  35833  bj-snglex  35843  bj-1uplth  35877  bj-1uplex  35878  bj-2uplth  35891  bj-2uplex  35892  bj-bm1.3ii  35934  bj-restpw  35962  bj-restuni  35967  bj-discrmoore  35981  bj-snmooreb  35984  bj-elid6  36040  bj-eldiag2  36047  mptsnunlem  36208  topdifinf  36219  elxp8  36241  finxp1o  36262  wl-moae  36374  wl-exeq  36392  wl-aleq  36393  wl-nfeqfb  36394  wl-ax11-lem6  36441  volsupnfl  36522  cover2  36572  isbnd3  36641  cntotbnd  36653  heibor  36678  isfld2  36862  isfldidl  36925  orfa  36939  eqbrb  37088  eqelb  37090  iss2  37202  issetssr  37362  n0el3  37510  detlem  37642  petlem  37671  prtlem16  37728  isltrn2N  38980  aks6d1c2p2  40946  sn-iotalem  41035  dffltz  41373  3cubes  41414  ismrc  41425  isnacs3  41434  rexzrexnn0  41528  eldioph4b  41535  dford3  41753  wopprc  41755  ttac  41761  pw2f1ocnv  41762  dfac11  41790  dfac21  41794  isnumbasabl  41834  isnumbasgrp  41835  dfacbasgrp  41836  aaitgo  41890  dflim5  42065  nvocnvb  42159  dfno2  42165  ifpbi1b  42240  rp-fakeimass  42249  rp-fakeanorass  42250  rp-isfinite5  42254  rp-isfinite6  42255  dfsucon  42260  snen1g  42261  iscard4  42270  rtrclex  42354  cnvtrrel  42407  frege54cor0a  42600  isotone1  42785  isotone2  42786  gneispace  42871  k0004lem3  42886  grumnueq  43032  ismnushort  43046  nanorxor  43050  nzss  43062  pm10.55  43114  pm11.57  43134  pm13.192  43155  pm13.194  43157  ipo0  43194  ifr0  43195  xpexb  43199  3impexpbicom  43226  com3rgbi  43261  pm2.43bgbi  43264  pm2.43cbi  43265  sb5ALT  43272  trsbc  43287  2pm13.193  43299  ax6e2ndeq  43306  2uasbanh  43308  eelT01  43458  eel0T1  43459  uunT1  43527  zfregs2VD  43588  equncomVD  43615  trsbcVD  43624  undif3VD  43629  2pm13.193VD  43650  ax6e2eqVD  43654  ax6e2ndeqVD  43656  2uasbanhVD  43658  ax6e2ndeqALT  43678  fompt  43876  mptssid  43930  elfzfzo  43973  allbutfi  44090  uzn0bi  44156  dvnprodlem3  44651  elaa2  44937  sge00  45079  elhoi  45245  ovn0  45269  ovolval4lem2  45353  confun  45636  afvfv0bi  45847  ffnafv  45866  afv2ndefb  45919  dfatafv2rnb  45922  afv2fv0b  45961  prpair  46156  sbcpr  46176  fpprel2  46396  sbgoldbmb  46441  mgm2mgm  46624  isringrng  46644  opprrngb  46662  nnpw2pb  47227  0aryfvalel  47274  mo0sn  47454  elsetrecs  47699  elpg  47713