Theorem impbii 201

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  dfbi1  205  bicom  214  biid  253  2th  256  pm5.74  262  bitri  267  notnotb  307  con34b  308  notbi  311  bibi2i  329  con1b  350  con2b  351  bi2.04  379  pm5.4  380  imdi  381  pm4.8  383  pm4.81  384  impexp  443  ancom  454  anass  462  jcab  513  orcom  859  dfor2  888  oridm  891  orbi2i  899  or12  907  biorfi  925  pm4.72  935  oibabs  937  jaob  947  pm4.44  982  pm4.79  989  andi  993  pm4.82  1009  cases2ALT  1032  consensus  1036  3impexp  1420  3jaob  1500  nanass  1580  nanassOLD  1581  tbw-bijust  1742  tbw-negdf  1743  19.26  1916  19.35  1924  19.21v  1982  19.23v  1985  19.41v  1992  sbbii  2019  19.9v  2030  equcom  2065  equvinvOLD  2078  equvelvOLD  2081  cbvalw  2085  alcom  2152  19.3  2186  19.41  2221  sb6  2250  sbimv  2280  cbvalv1  2312  cbval  2368  cbvalv  2370  equsex  2383  aecom  2393  equs45f  2425  dfsb2  2449  sb6f  2461  sbim  2471  sb6OLD  2506  moabs  2555  mo3  2580  mo3OLD  2581  exmoeu  2601  dfmo  2615  moeuOLD  2618  dfeuOLD  2630  exmoeuOLD  2632  moanimlem  2653  euan  2656  euanv  2660  2mo  2678  2eu6  2687  euae  2690  axext4  2758  eqcom  2785  nebi  3049  r19.26  3250  ralcom3  3291  ceqsex  3443  gencbvex  3452  gencbvex2  3453  clel5OLD  3548  pm13.183  3549  pm13.183OLD  3550  rr19.3v  3551  rr19.28v  3552  euxfr2  3603  reu6  3607  reu3  3608  sspss  3928  complss  3974  unineq  4104  uneqin  4105  difrab  4127  sbnfc2  4233  un00  4237  ssdifeq0  4275  r19.2zb  4284  snidb  4429  rabsnifsb  4489  tppreqb  4567  difsnb  4568  pwpw0  4575  sssn  4588  preq12b  4610  pwsnALT  4664  unissint  4734  uniintsn  4747  iununi  4844  al0ssb  5027  intex  5054  intnex  5055  iin0  5073  axpweq  5076  nfcvb  5088  eusvnfb  5105  eusv2nf  5107  ralxfrALT  5127  sspwb  5149  unipw  5150  opnz  5173  opth  5176  opeqsng  5198  propeqop  5204  opthwiener  5211  opthhausdorff  5214  opthhausdorff0  5215  ssopab2b  5239  pwssun  5257  opelxp  5391  opthprc  5413  relsnb  5473  relop  5518  issetid  5522  xpid11  5592  elinxp  5683  elresOLD  5685  eldmeldmressn  5690  iss  5697  idrefOLD  5764  asymref2  5768  xpnz  5807  xpdifid  5816  ssrnres  5826  dfrel2  5837  relrelss  5913  unixp0  5923  fn0  6257  funssxp  6311  f00  6337  f0bi  6338  dffo2  6370  f1o00  6425  fo00  6426  fv3  6464  dffn5  6501  dff2  6635  dff3  6636  dffo4  6639  dffo5  6640  exfo  6641  fmpt  6644  ffnfv  6652  fsn  6667  fsn2  6668  funop  6680  funsneqopb  6685  fnsnb  6699  isores1  6856  ssoprab2b  6989  eqfnov2  7044  unexb  7235  uniexb  7250  pwexb  7252  iunpw  7256  ordeleqon  7266  onintrab  7279  unon  7309  onuninsuci  7318  ordzsl  7323  onzsl  7324  f1oexbi  7395  ffoss  7406  1st2ndb  7485  suppssov1  7609  suppssfv  7613  reldmtpos  7642  dfrecs3  7752  omopthi  8021  ecopover  8135  mapsncnv  8190  mptelixpg  8231  elixpsn  8233  ixpsnf1o  8234  bren2  8272  en0  8304  en1  8308  en1b  8309  sbthb  8369  canth2  8401  onfin2  8440  sdom1  8448  1sdom  8451  fineqv  8463  unfilem1  8512  fiint  8525  residfi  8535  pwfi  8549  unifpw  8557  wofib  8739  sucprcreg  8795  opthreg  8810  opthregOLD  8812  suc11reg  8813  infeq5  8831  rankwflemb  8953  r1elss  8966  pwwf  8967  unwf  8970  uniwf  8979  rankonid  8989  rankr1id  9022  rankuni  9023  rankxplim3  9041  scott0  9046  karden  9055  isnum3  9113  oncard  9119  card1  9127  cardlim  9131  cardmin2  9157  pm54.43lem  9158  ween  9191  acnnum  9208  alephsuc2  9236  alephgeom  9238  iscard3  9249  dfac3  9277  dfac4  9278  dfac5lem3  9281  dfac5  9284  dfac2  9287  dfac2OLD  9288  dfac8  9292  dfac9  9293  dfacacn  9298  dfac13  9299  dfac12r  9303  dfac12k  9304  kmlem2  9308  kmlem13  9319  cdainf  9349  ackbij2  9400  cflim2  9420  isfin4-2  9471  isfin4-3  9472  isf33lem  9523  compsscnv  9528  fin1a2lem6  9562  domtriom  9600  ac9  9640  ac9s  9650  fodomb  9683  brdom3  9685  brdom5  9686  brdom4  9687  brdom7disj  9688  brdom6disj  9689  iunfo  9696  sdomsdomcard  9717  gch2  9832  gch3  9833  eltsk2g  9908  grutsk  9979  ordpipq  10099  ltbtwnnq  10135  mappsrpr  10265  map2psrpr  10267  elreal2  10289  le2tri3i  10506  elnn0nn  11686  elnnnn0b  11688  elnnnn0c  11689  elnnz  11738  elnn0z  11741  elz2  11745  elnnz1  11755  eluz2b2  12068  elnn1uz2  12072  elpqb  12123  elioo4g  12546  eluzfz2b  12667  fzn0  12672  elfz1end  12688  fzass4  12696  elfz1b  12727  nn0fz0  12756  fzolb  12795  fzon0  12806  elfzo0  12828  elfzo0z  12829  elfzo1  12837  fzo1fzo0n0  12838  om2uzrani  13070  nn0opthi  13375  hashkf  13437  isfinite4  13468  hashprb  13499  hashf1  13555  elss2prb  13583  iswrdb  13605  wrdexb  13611  0wrd0  13628  wrdl3s3  14114  cotr2g  14124  trclun  14162  sqr0lem  14388  rexanuz  14492  rexuz3  14495  fsum0diag  14913  fprod0diag  15119  divalgmod  15536  sadcp1  15583  isprm6  15830  nnoddn2prmb  15922  4sqlem4  16060  mreunirn  16647  isdrs2  17325  isacs5  17558  isacs4  17559  isacs3  17560  dfgrp2  17834  dfgrp3  17901  dfgrp3e  17902  isnsg3  18012  gicer  18102  oppgmndb  18168  oppggrpb  18171  pmtrfb  18268  invghm  18625  opprringb  19019  isnzr2hash  19661  abvn0b  19699  gzrngunit  20208  dvdsrzring  20227  zringunit  20232  zlmlmod  20267  zlmassa  20268  cygth  20315  frgpcyg  20317  toprntopon  21137  tgclb  21182  iscldtop  21307  isnrm2  21570  isnrm3  21571  discmp  21610  dfconn2  21631  2ndcsb  21661  dis2ndc  21672  loclly  21699  unisngl  21739  locfindis  21742  iskgen2  21760  dfac14  21830  kqtop  21957  kqt0  21958  kqreg  21963  kqnrm  21964  hmpher  21996  hmphsymb  21998  hmph0  22007  kqhmph  22031  ist1-5lem  22032  elmptrab2  22040  isfil2  22068  filunirn  22094  isufil2  22120  hausflim  22193  isfcls  22221  alexsubALT  22263  istgp2  22303  ustbas  22439  xmetunirn  22550  dscmet  22785  dscopn  22786  isngp4  22824  zcld  23024  zlmclm  23319  iscmet2  23500  iundisj  23752  i1f1lem  23893  fta1b  24366  elply2  24389  elqaa  24514  aannenlem2  24521  wilth  25249  lgsne0  25512  2lgs  25584  2sqlem2  25595  ostth  25780  mptelee  26244  wrdupgr  26433  wrdumgr  26445  umgrislfupgr  26471  uspgrupgrushgr  26526  usgrumgruspgr  26529  usgruspgrb  26530  usgrislfuspgr  26533  uvtx01vtx  26745  wwlksnwwlksnon  27295  elwwlks2ons3  27335  clwwlkn1loopb  27433  eclclwwlkn1  27473  upgriseupth  27610  numclwwlkovh  27801  nmlno0lem  28220  isblo3i  28228  blocni  28232  hvsubeq0i  28492  hvaddcani  28494  bcseqi  28549  isch3  28670  norm1exi  28679  hhsssh  28698  shslubi  28816  dfch2  28838  pjoc1i  28862  pjchi  28863  shs00i  28881  chsscon3i  28892  chlejb1i  28907  chj00i  28918  shjshseli  28924  h1de2ctlem  28986  spanunsni  29010  cmcmi  29023  cmbr3i  29031  cmbr4i  29032  pj11i  29142  hosubeq0i  29257  dmadjrnb  29337  nmlnop0iALT  29426  lnopeq0i  29438  elunop2  29444  lnconi  29464  lncnopbd  29468  adjbdlnb  29515  adjbd1o  29516  adjeq0  29522  rnbra  29538  pjss1coi  29594  pjss2coi  29595  pjnormssi  29599  pjssdif2i  29605  pjssdif1i  29606  dfpjop  29613  pjinvari  29622  pjin2i  29624  pjci  29631  pjcmul1i  29632  pjcmul2i  29633  strb  29689  hstrbi  29697  mdsl1i  29752  atom1d  29784  chrelat2i  29796  cvbr4i  29798  cvexchi  29800  sumdmdi  29851  dmdbr4ati  29852  dmdbr5ati  29853  dmdbr6ati  29854  dmdbr7ati  29855  cdj3i  29872  difeq  29917  iundisjf  29965  cnvoprabOLD  30064  fpwrelmap  30074  iundisjfi  30119  xrge0tsmsbi  30348  issgon  30784  measbasedom  30863  oddpwdc  31014  eulerpartlemt  31031  ballotlem2  31149  ballotlemrinv  31194  bnj1533  31521  bnj983  31620  elmsta  32044  nepss  32196  dford5  32205  dfpo2  32239  dfon2  32285  distel  32297  elno2  32396  bdayfo  32417  fnimage  32625  altopthsn  32657  ellines  32848  rankeq1o  32867  opnrebl2  32904  df3nandALT1  32982  bj-dfbi6  33138  bj-consensus  33141  bj-falor2  33149  bj-bibibi  33150  bj-andnotim  33152  bj-cbval  33204  bj-cbvex  33205  bj-ssbeq  33218  bj-ssb0  33219  bj-19.41al  33227  bj-sb56  33229  bj-eqs  33252  bj-cbvexw  33253  bj-sb  33266  bj-equs45fv  33337  bj-sbfvv  33344  bj-axext4  33347  bj-hbaeb2  33380  bj-hbnaeb  33382  bj-equsal  33388  bj-sbsb  33399  bj-moeub  33405  bj-mo3OLD  33407  bj-cleqhyp  33463  bj-csbsnlem  33469  bj-snsetex  33523  bj-snglex  33533  bj-1uplth  33567  bj-1uplex  33568  bj-2uplth  33581  bj-2uplex  33582  bj-bm1.3ii  33596  bj-restpw  33618  bj-restuni  33623  bj-ismooredr2  33638  bj-discrmoore  33639  bj-snmoore  33641  bj-elid  33663  bj-elid3  33665  bj-eldiag2  33671  mptsnunlem  33781  topdifinf  33792  elxp8  33814  finxp1o  33824  wl-moae  33894  wl-nfnbi  33908  wl-exeq  33915  wl-aleq  33916  wl-nfeqfb  33917  wl-dv-sb  33924  wl-ax11-lem6  33961  volsupnfl  34080  cover2  34133  isbnd3  34207  cntotbnd  34219  heibor  34244  isfld2  34428  isfldidl  34491  orfa  34505  eqelb  34640  iss2  34740  issetssr  34881  prtlem16  35023  isltrn2N  36274  brabg2a  38123  dffltz  38213  ismrc  38224  isnacs3  38233  rexzrexnn0  38328  eldioph4b  38335  dford3  38554  wopprc  38556  ttac  38562  pw2f1ocnv  38563  dfac11  38591  dfac21  38595  isnumbasabl  38635  isnumbasgrp  38636  dfacbasgrp  38637  aaitgo  38691  ifpbi1b  38806  rp-fakeimass  38815  rp-fakeanorass  38816  rp-isfinite5  38820  rp-isfinite6  38821  rtrclex  38881  cnvtrrel  38919  rp-imass  39021  frege54cor0a  39113  isotone1  39302  isotone2  39303  gneispace  39388  k0004lem3  39403  nanorxor  39460  nzss  39472  pm10.55  39524  pm11.57  39545  pm13.192  39566  pm13.194  39568  ipo0  39607  ifr0  39608  xpexb  39612  3impexpbicom  39639  com3rgbi  39674  pm2.43bgbi  39677  pm2.43cbi  39678  sb5ALT  39685  trsbc  39700  2pm13.193  39712  ax6e2ndeq  39719  2uasbanh  39721  eelT01  39880  eel0T1  39881  uunT1  39949  zfregs2VD  40010  equncomVD  40037  trsbcVD  40046  undif3VD  40051  2pm13.193VD  40072  ax6e2eqVD  40076  ax6e2ndeqVD  40078  2uasbanhVD  40080  ax6e2ndeqALT  40100  fompt  40302  mptssid  40364  elfzfzo  40398  allbutfi  40522  uzn0bi  40594  dvnprodlem3  41091  elaa2  41378  sge00  41517  ismea  41592  elhoi  41683  ovn0  41707  ovolval4lem2  41791  confun  42033  reuan  42138  afvfv0bi  42193  ffnafv  42212  afv2ndefb  42265  dfatafv2rnb  42268  afv2fv0b  42307  prpair  42440  sbgoldbmb  42699  mgm2mgm  42878  isringrng  42896  nnpw2pb  43396  elsetrecs  43551  elpg  43565