Theorem impbii 209

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bicom  222  biid  261  2th  264  pm5.74  270  bitri  275  notnotb  315  con34b  316  notbi  319  bibi2i  337  con1b  358  con2b  359  bi2.04  387  imdi  389  pm4.8  392  pm4.81  393  impexp  450  ancom  460  anass  468  jcab  517  impimprbi  829  orcom  870  dfor2  901  oridm  904  orbi2i  912  or12  920  biorfriOLD  940  pm4.72  951  oibabs  953  jaob  963  pm4.44  998  pm4.79  1005  andi  1009  pm4.82  1025  cases2ALT  1048  consensus  1052  3impexp  1357  3jaobOLD  1426  nanass  1506  tbw-bijust  1694  tbw-negdf  1695  19.26  1867  19.35  1874  19.21v  1936  19.23v  1939  19.41v  1946  19.3v  1978  19.9v  1980  equcom  2014  cbvalw  2031  alcomw  2041  exexw  2048  sbbii  2073  sban  2077  sbv  2085  alcom  2156  19.3  2199  19.41  2232  sbalex  2239  sbalexOLD  2240  equsexv  2265  sbim  2301  cbvalv1  2341  cbval  2400  equsex  2420  aecom  2429  equs45f  2461  dfsb1  2483  dfsb2  2495  sb6f  2499  dfmoeu  2533  moabs  2540  mobii  2545  mo3  2561  mo4  2563  exmoeu  2578  moanimlem  2615  euan  2618  euanv  2621  2mo  2645  2eu6  2654  euae  2657  axextb  2708  eqcom  2741  nebi  3018  ralcom3OLD  3095  r19.35  3105  r19.35OLD  3106  r19.26  3108  r19.21v  3177  ceqsexOLD  3528  ceqsexvOLD  3530  gencbvex  3540  gencbvex2  3541  pm13.183  3665  rr19.3v  3666  rr19.28v  3667  euxfr2w  3728  euxfr2  3730  reu6  3734  reu3  3735  reuan  3904  dfss2  3980  sspss  4111  complss  4160  unineq  4293  uneqin  4294  difrab  4323  ab0w  4384  sbnfc2  4444  un00  4450  disj  4455  ssdifeq0  4492  r19.2zb  4501  ralidmw  4513  ralidm  4517  ralf0  4519  pwidb  4625  snidb  4665  rabsnifsb  4726  tppreqb  4809  difsnb  4810  pwpw0  4817  sssn  4830  preq12b  4854  unissint  4976  uniintsn  4989  iununi  5103  al0ssb  5313  intex  5349  intnex  5350  axpweq  5356  iin0  5367  nfcvb  5381  eusvnfb  5398  eusv2nf  5400  ralxfrALT  5420  sspwb  5459  unipw  5460  opnz  5483  opth  5486  sbcop1  5498  opeqsng  5512  propeqop  5516  opthwiener  5523  opthhausdorff  5526  opthhausdorff0  5527  rexopabb  5537  ssopab2bw  5556  ssopab2b  5558  pwssun  5579  opelxp  5724  opthprc  5752  relsnb  5814  relop  5863  issetid  5867  xpid11  5945  elinxp  6038  eldmeldmressn  6044  iss  6054  iresn0n0  6073  asymref2  6139  xpnz  6180  xpdifid  6189  ssrnres  6199  dfrel2  6210  resssxp  6291  relrelss  6294  unixp0  6304  reuop  6314  dfpo2  6317  fn0  6699  funssxp  6764  f00  6790  f0bi  6791  dffo2  6824  f1o00  6883  fo00  6884  fv3  6924  dffn5  6966  dff2  7118  dff3  7119  dffo4  7122  dffo5  7123  exfo  7124  fmpt  7129  fompt  7137  ffnfv  7138  fsn  7154  fsn2  7155  funop  7168  funsneqopb  7171  fnsnb  7185  isores1  7353  ssoprab2b  7501  eqoprab2bw  7502  eqfnov2  7562  unexb  7765  unexbOLD  7766  uniexb  7782  pwexb  7784  iunpw  7789  ordeleqon  7800  dford5  7802  onintrab  7815  ordsuc  7832  unon  7850  onuninsuci  7860  ordzsl  7865  onzsl  7866  f1oexbi  7950  ffoss  7968  1st2ndb  8052  frxp3  8174  suppssov1  8220  suppssov2  8221  suppssfv  8225  reldmtpos  8257  dfrecs3  8410  dfrecs3OLD  8411  omopthi  8697  brinxper  8772  ecopover  8859  fsetexb  8902  mapsncnv  8931  mptelixpg  8973  elixpsn  8975  ixpsnf1o  8976  bren2  9021  en0  9056  en0ALT  9057  en0r  9058  en1  9062  en1b  9063  sbthb  9132  dom0  9140  canth2  9168  onfin2  9265  sdom1  9275  sdom1OLD  9276  1sdom2dom  9280  1sdomOLD  9282  fineqv  9296  unfilem1  9340  unfib  9344  pwfir  9352  pwfi  9354  fiint  9363  fiintOLD  9364  residfi  9375  unifpw  9392  wofib  9582  sucprcreg  9638  opthreg  9655  suc11reg  9656  infeq5  9674  rankwflemb  9830  r1elss  9843  pwwf  9844  unwf  9847  uniwf  9856  rankonid  9866  rankr1id  9899  rankuni  9900  rankxplim3  9918  scott0  9923  karden  9932  djuexb  9946  isnum3  9991  oncard  9997  card1  10005  cardlim  10009  cardmin2  10036  pm54.43lem  10037  ween  10072  acnnum  10089  alephsuc2  10117  alephgeom  10119  iscard3  10130  dfac3  10158  dfac4  10159  dfac5lem3  10162  dfac5  10166  dfac2  10169  dfac8  10173  dfac9  10174  dfacacn  10179  dfac13  10180  dfac12r  10184  dfac12k  10185  kmlem2  10189  kmlem13  10200  djuinf  10226  ackbij2  10279  cflim2  10300  isfin4-2  10351  isfin4p1  10352  isf33lem  10403  compsscnv  10408  fin1a2lem6  10442  domtriom  10480  ac9  10520  ac9s  10530  fodomb  10563  brdom3  10565  brdom5  10566  brdom4  10567  brdom7disj  10568  brdom6disj  10569  iunfo  10576  sdomsdomcard  10597  gch2  10712  gch3  10713  eltsk2g  10788  grutsk  10859  ordpipq  10979  ltbtwnnq  11015  mappsrpr  11145  map2psrpr  11147  elreal2  11169  le2tri3i  11388  elnn0nn  12565  elnnnn0b  12567  elnnnn0c  12568  elnnz  12620  elnn0z  12623  elz2  12628  elnnz1  12640  eluz2b2  12960  elnn1uz2  12964  elpqb  13015  elioo4g  13443  eluzfz2b  13569  fzn0  13574  elfz1end  13590  fzass4  13598  elfz1b  13629  nn0fz0  13661  fzolb  13701  fzon0  13713  elfzo0  13736  elfzo0z  13737  elfzo1  13748  fzo1fzo0n0  13750  om2uzrani  13989  nn0opthi  14305  hashkf  14367  isfinite4  14397  hashprb  14432  hashf1  14492  elss2prb  14523  iswrdb  14554  wrdexb  14559  0wrd0  14574  wrdl3s3  14997  cotr2g  15011  trclun  15049  rexanuz  15380  rexuz3  15383  fsum0diag  15809  fprod0diag  16018  divalgmod  16439  sadcp1  16488  isprm6  16747  nnoddn2prmb  16846  4sqlem4  16985  fnpr2ob  17604  mreunirn  17645  isdrs2  18363  isacs5  18605  isacs4  18606  isacs3  18607  dfgrp2  18992  dfgrp3  19069  dfgrp3e  19070  isnsg3  19190  gicer  19307  oppgmndb  19388  oppggrpb  19391  pmtrfb  19497  invghm  19865  isringrng  20300  opprrngb  20362  opprringb  20364  isnzr2hash  20535  isdomn4  20732  abvn0b  20853  gzrngunit  21468  dvdsrzring  21489  zringunit  21494  zlmlmod  21554  cygth  21607  frgpcyg  21609  zlmassa  21940  toprntopon  22946  tgclb  22992  iscldtop  23118  isnrm2  23381  isnrm3  23382  discmp  23421  dfconn2  23442  2ndcsb  23472  dis2ndc  23483  loclly  23510  unisngl  23550  locfindis  23553  iskgen2  23571  dfac14  23641  kqtop  23768  kqt0  23769  kqreg  23774  kqnrm  23775  hmpher  23807  hmphsymb  23809  hmph0  23818  kqhmph  23842  ist1-5lem  23843  elmptrab2  23851  isfil2  23879  filunirn  23905  isufil2  23931  hausflim  24004  isfcls  24032  alexsubALT  24074  istgp2  24114  ustbas  24251  xmetunirn  24362  dscmet  24600  dscopn  24601  isngp4  24640  zcld  24848  zlmclm  25158  iscmet2  25341  iundisj  25596  i1f1lem  25737  fta1b  26225  elply2  26249  elqaa  26378  aannenlem2  26385  wilth  27128  lgsne0  27393  2lgs  27465  2sqlem2  27476  ostth  27697  elno2  27713  bdayfo  27736  elons2  28295  eln0s  28372  elzn0s  28398  eln0zs  28400  elnnzs  28401  remulscllem1  28446  mptelee  28924  wrdupgr  29116  wrdumgr  29128  umgrislfupgr  29154  uspgrupgrushgr  29210  usgrumgruspgr  29213  usgruspgrb  29214  usgrislfuspgr  29218  uvtx01vtx  29428  wwlksnwwlksnon  29944  elwwlks2ons3  29984  clwwlkn1loopb  30071  eclclwwlkn1  30103  upgriseupth  30235  numclwwlkovh  30401  nmlno0lem  30821  isblo3i  30829  blocni  30833  hvsubeq0i  31091  hvaddcani  31093  bcseqi  31148  isch3  31269  norm1exi  31278  hhsssh  31297  shslubi  31413  dfch2  31435  pjoc1i  31459  pjchi  31460  shs00i  31478  chsscon3i  31489  chlejb1i  31504  chj00i  31515  shjshseli  31521  h1de2ctlem  31583  spanunsni  31607  cmcmi  31620  cmbr3i  31628  cmbr4i  31629  pj11i  31739  hosubeq0i  31854  dmadjrnb  31934  nmlnop0iALT  32023  lnopeq0i  32035  elunop2  32041  lnconi  32061  lncnopbd  32065  adjbdlnb  32112  adjbd1o  32113  adjeq0  32119  rnbra  32135  pjss1coi  32191  pjss2coi  32192  pjnormssi  32196  pjssdif2i  32202  pjssdif1i  32203  dfpjop  32210  pjinvari  32219  pjin2i  32221  pjci  32228  pjcmul1i  32229  pjcmul2i  32230  strb  32286  hstrbi  32294  mdsl1i  32349  atom1d  32381  chrelat2i  32393  cvbr4i  32395  cvexchi  32397  sumdmdi  32448  dmdbr4ati  32449  dmdbr5ati  32450  dmdbr6ati  32451  dmdbr7ati  32452  cdj3i  32469  eqtrb  32501  difeq  32545  iundisjf  32608  cnvoprabOLD  32737  fpwrelmap  32750  iundisjfi  32803  xrge0tsmsbi  33048  dfufd2  33557  ccfldextdgrr  33696  issgon  34103  measbasedom  34182  oddpwdc  34335  eulerpartlemt  34352  ballotlem2  34469  ballotlemrinv  34514  bnj1533  34844  bnj983  34943  0nn0m1nnn0  35096  lfuhgr3  35103  spthcycl  35113  satfv1  35347  satf0op  35361  fmla0xp  35367  fmla1  35371  elmsta  35532  nepss  35697  dfon2  35773  distel  35784  fnimage  35910  altopthsn  35942  ellines  36133  rankeq1o  36152  opnrebl2  36303  df3nandALT1  36381  bj-animbi  36541  bj-dfbi6  36557  bj-consensus  36560  bj-falor2  36567  bj-bibibi  36568  bj-andnotim  36570  bj-cbval  36631  bj-cbvex  36632  bj-ssbeq  36635  bj-19.41al  36641  bj-subst  36643  bj-eqs  36657  bj-cbvexw  36658  bj-sb  36669  bj-substax12  36703  bj-dfnnf3  36739  bj-equs45fv  36793  bj-hbaeb2  36800  bj-hbnaeb  36802  bj-equsal  36808  bj-sbsb  36819  bj-moeub  36831  bj-csbsnlem  36885  bj-snsetex  36945  bj-snglex  36955  bj-1uplth  36989  bj-1uplex  36990  bj-2uplth  37003  bj-2uplex  37004  bj-bm1.3ii  37046  bj-restpw  37074  bj-restuni  37079  bj-discrmoore  37093  bj-snmooreb  37096  bj-elid6  37152  bj-eldiag2  37159  mptsnunlem  37320  topdifinf  37331  elxp8  37353  finxp1o  37374  wl-moae  37496  wl-exeq  37514  wl-aleq  37515  wl-nfeqfb  37516  wl-ax11-lem6  37570  volsupnfl  37651  cover2  37701  isbnd3  37770  cntotbnd  37782  heibor  37807  isfld2  37991  isfldidl  38054  orfa  38068  eqbrb  38213  eqelb  38215  iss2  38325  issetssr  38484  n0el3  38632  detlem  38764  petlem  38793  prtlem16  38850  isltrn2N  40102  aks6d1c2p2  42100  aks6d1c6isolem3  42157  sn-iotalem  42238  dffltz  42620  eu6w  42662  3cubes  42677  ismrc  42688  isnacs3  42697  rexzrexnn0  42791  eldioph4b  42798  dford3  43016  wopprc  43018  ttac  43024  pw2f1ocnv  43025  dfac11  43050  dfac21  43054  isnumbasabl  43094  isnumbasgrp  43095  dfacbasgrp  43096  aaitgo  43150  dflim5  43318  nvocnvb  43411  dfno2  43417  ifpbi1b  43492  rp-fakeimass  43501  rp-fakeanorass  43502  rp-isfinite5  43506  rp-isfinite6  43507  dfsucon  43512  snen1g  43513  iscard4  43522  rtrclex  43606  cnvtrrel  43659  frege54cor0a  43852  isotone1  44037  isotone2  44038  gneispace  44123  k0004lem3  44138  grumnueq  44282  ismnushort  44296  nanorxor  44300  nzss  44312  pm10.55  44364  pm11.57  44384  pm13.192  44405  pm13.194  44407  ipo0  44444  ifr0  44445  xpexb  44449  3impexpbicom  44476  com3rgbi  44511  pm2.43bgbi  44514  pm2.43cbi  44515  sb5ALT  44522  trsbc  44537  2pm13.193  44549  ax6e2ndeq  44556  2uasbanh  44558  eelT01  44708  eel0T1  44709  uunT1  44777  zfregs2VD  44838  equncomVD  44865  trsbcVD  44874  undif3VD  44879  2pm13.193VD  44900  ax6e2eqVD  44904  ax6e2ndeqVD  44906  2uasbanhVD  44908  ax6e2ndeqALT  44928  mptssid  45184  elfzfzo  45226  allbutfi  45342  uzn0bi  45408  dvnprodlem3  45903  elaa2  46189  sge00  46331  elhoi  46497  ovn0  46521  ovolval4lem2  46605  confun  46888  afvfv0bi  47101  ffnafv  47120  afv2ndefb  47173  dfatafv2rnb  47176  afv2fv0b  47215  prpair  47425  sbcpr  47445  fpprel2  47665  sbgoldbmb  47710  vopnbgrelself  47778  isgrtri  47847  stgr1  47863  mgm2mgm  48070  nnpw2pb  48436  0aryfvalel  48483  mo0sn  48663  elsetrecs  48930  elpg  48944