Theorem impbii 199

Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 198. (Contributed by NM, 29-Dec-1992.)

Hypotheses

Ref	Expression
impbii.1	|- ( ph -> ps )
impbii.2	|- ( ps -> ph )

Assertion

Ref	Expression
impbii	|- ( ph <-> ps )

Proof of Theorem impbii

Step	Hyp	Ref	Expression
1		impbii.1	. 2 |- ( ph -> ps )
2		impbii.2	. 2 |- ( ps -> ph )
3		impbi 198	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 9	1 |- ( ph <-> ps )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  dfbi1  203  bicom  212  biid  251  2th  254  pm5.74  259  bitri  264  notnotb  304  con34b  306  notbi  309  bibi2i  327  con1b  348  con2b  349  bi2.04  376  pm5.4  377  imdi  378  pm4.8  380  pm4.81  381  orcom  402  biorfi  422  dfor2  427  impexp  462  ancom  466  oridm  536  orbi2i  541  or12  545  pm4.45im  585  pm4.44  601  pm4.79  607  anass  681  jaob  822  jcab  907  andi  911  pm4.72  920  oibabs  925  pm4.82  969  cases2  993  consensus  999  3impexp  1289  3jaob  1390  tbw-bijust  1623  tbw-negdf  1624  19.26  1798  19.35  1805  19.21v  1868  sbbii  1887  19.9v  1896  19.23v  1902  19.41v  1914  equcom  1945  equvinv  1959  equvinvOLD  1962  equvelv  1963  cbvalw  1968  alcom  2037  19.3  2069  19.41  2103  cbvalv1  2175  19.3OLD  2202  cbval  2271  cbvalv  2273  equsex  2292  aecom  2311  equs45f  2350  dfsb2  2373  sb6f  2385  sbim  2395  sb6  2429  mo2v  2477  exmoeu  2502  mo3  2507  moanim  2529  euan  2530  2mo  2551  2eu6  2558  axext4  2606  eqcom  2629  nebi  2874  r19.26  3064  ralcom3  3105  ceqsex  3241  gencbvex  3250  gencbvex2  3251  clel5  3343  pm13.183  3344  rr19.3v  3345  rr19.28v  3346  euxfr2  3391  reu6  3395  reu3  3396  sspss  3706  complss  3751  unineq  3877  uneqin  3878  undif3OLD  3889  difrab  3901  sbnfc2  4007  un00  4011  ssdifeq0  4051  r19.2zb  4061  ralf0OLD  4079  elpr2OLD  4200  snidb  4207  rabsnifsb  4257  ssdifsn  4318  tppreqb  4336  difsnb  4337  pwpw0  4344  sssn  4358  preq12b  4382  preqsnOLD  4394  pwsnALT  4429  unissint  4501  uniintsn  4514  iununi  4610  intex  4820  intnex  4821  iin0  4839  axpweq  4842  eusvnfb  4862  eusv2nf  4864  ralxfrALT  4887  nfcvb  4898  sspwb  4917  unipw  4918  opnz  4942  opth  4945  propeqop  4970  opthwiener  4976  ssopab2b  5002  pwssun  5020  opelxp  5146  opthprc  5167  relop  5272  issetid  5276  xpid11  5347  elres  5435  eldmeldmressn  5440  iss  5447  restidsingOLD  5459  issref  5509  asymref2  5513  xpnz  5553  xpdifid  5562  ssrnres  5572  dfrel2  5583  relrelss  5659  unixp0  5669  fn0  6011  funssxp  6061  f00  6087  f0bi  6088  dffo2  6119  f1o00  6171  fo00  6172  fv3  6206  dffn5  6241  dff2  6371  dff3  6372  dffo4  6375  dffo5  6376  exfo  6377  fmpt  6381  ffnfv  6388  fsn  6402  fsn2  6403  funop  6414  funsneqopb  6419  fnsnb  6432  isores1  6584  ssoprab2b  6712  eqfnov2  6767  unexb  6958  uniexb  6973  pwexb  6975  iunpw  6978  ordeleqon  6988  onintrab  7001  unon  7031  onuninsuci  7040  ordzsl  7045  onzsl  7046  f1oexbi  7116  ffoss  7127  1st2ndb  7206  suppssov1  7327  suppssfv  7331  reldmtpos  7360  dfrecs3  7469  omopthi  7737  ecopover  7851  mapsn  7899  mapsncnv  7904  mptelixpg  7945  elixpsn  7947  ixpsnf1o  7948  bren2  7986  en0  8019  en1  8023  en1b  8024  sbthb  8081  canth2  8113  onfin2  8152  sdom1  8160  1sdom  8163  fineqv  8175  unfilem1  8224  fiint  8237  residfi  8247  pwfi  8261  unifpw  8269  wofib  8450  sucprcreg  8506  opthreg  8515  suc11reg  8516  infeq5  8534  rankwflemb  8656  r1elss  8669  pwwf  8670  unwf  8673  uniwf  8682  rankonid  8692  rankr1id  8725  rankuni  8726  rankxplim3  8744  scott0  8749  karden  8758  isnum3  8780  oncard  8786  card1  8794  cardlim  8798  cardmin2  8824  pm54.43lem  8825  ween  8858  acnnum  8875  alephsuc2  8903  alephgeom  8905  iscard3  8916  dfac3  8944  dfac4  8945  dfac5lem3  8948  dfac5  8951  dfac2  8953  dfac8  8957  dfac9  8958  dfacacn  8963  dfac13  8964  dfac12r  8968  dfac12k  8969  kmlem2  8973  kmlem13  8984  cdainf  9014  ackbij2  9065  cflim2  9085  isfin4-2  9136  isfin4-3  9137  isf33lem  9188  compsscnv  9193  fin1a2lem6  9227  domtriom  9265  ac9  9305  ac9s  9315  fodomb  9348  brdom3  9350  brdom5  9351  brdom4  9352  brdom7disj  9353  brdom6disj  9354  iunfo  9361  sdomsdomcard  9382  gch2  9497  gch3  9498  eltsk2g  9573  grutsk  9644  grothpw  9648  ordpipq  9764  ltbtwnnq  9800  mappsrpr  9929  map2psrpr  9931  elreal2  9953  le2tri3i  10167  elnn0nn  11335  elnnnn0b  11337  elnnnn0c  11338  elnnz  11387  elnn0z  11390  elz2  11394  elnnz1  11403  eluz2b2  11761  elnn1uz2  11765  elioo4g  12234  eluzfz2b  12350  fzn0  12355  elfz1end  12371  fzass4  12379  elfz1b  12409  nn0fz0  12437  fzolb  12476  fzon0  12487  elfzo0  12508  elfzo0z  12509  elfzo1  12517  fzo1fzo0n0  12518  om2uzrani  12751  nn0opthi  13057  hashkf  13119  isfinite4  13153  hashprb  13185  hashf1  13241  elss2prb  13269  iswrdb  13311  wrdexb  13316  0wrd0  13331  wrdl3s3  13705  cotr2g  13715  trclun  13755  sqr0lem  13981  rexanuz  14085  rexuz3  14088  fsum0diag  14509  fprod0diag  14717  divalgmod  15129  sadcp1  15177  isprm6  15426  nnoddn2prmb  15518  4sqlem4  15656  mreunirn  16261  isdrs2  16939  isacs5  17172  isacs4  17173  isacs3  17174  dfgrp2  17447  dfgrp3  17514  dfgrp3e  17515  isnsg3  17628  gicer  17718  gicerOLD  17719  oppgmndb  17785  oppggrpb  17788  pmtrfb  17885  invghm  18239  opprringb  18632  isnzr2hash  19264  abvn0b  19302  gzrngunit  19812  dvdsrzring  19831  zringunit  19836  zlmlmod  19871  zlmassa  19872  cygth  19920  frgpcyg  19922  toprntopon  20729  tgclb  20774  iscldtop  20899  isnrm2  21162  isnrm3  21163  discmp  21201  dfconn2  21222  2ndcsb  21252  dis2ndc  21263  loclly  21290  unisngl  21330  locfindis  21333  iskgen2  21351  dfac14  21421  kqtop  21548  kqt0  21549  kqreg  21554  kqnrm  21555  hmpher  21587  hmphsymb  21589  hmph0  21598  kqhmph  21622  ist1-5lem  21623  elmptrab2OLD  21631  elmptrab2  21632  isfil2  21660  filunirn  21686  isufil2  21712  hausflim  21785  isfcls  21813  alexsubALT  21855  istgp2  21895  ustbas  22031  xmetunirn  22142  dscmet  22377  dscopn  22378  isngp4  22416  zcld  22616  zlmclm  22912  iscmet2  23092  iundisj  23316  i1f1lem  23456  fta1b  23929  elply2  23952  elqaa  24077  aannenlem2  24084  wilth  24797  lgsne0  25060  2lgs  25132  2sqlem2  25143  ostth  25328  mptelee  25775  wrdupgr  25980  wrdumgr  25992  umgrislfupgr  26018  uspgrupgrushgr  26072  usgrumgruspgr  26075  usgruspgrb  26076  usgrislfuspgr  26079  uvtxa01vtx0  26297  clwwlknclwwlkdifs  26873  eclclwwlksn1  26952  upgriseupth  27067  nmlno0lem  27648  isblo3i  27656  blocni  27660  hvsubeq0i  27920  hvaddcani  27922  bcseqi  27977  isch3  28098  norm1exi  28107  hhsssh  28126  shslubi  28244  dfch2  28266  pjoc1i  28290  pjchi  28291  shs00i  28309  chsscon3i  28320  chlejb1i  28335  chj00i  28346  shjshseli  28352  h1de2ctlem  28414  spanunsni  28438  cmcmi  28451  cmbr3i  28459  cmbr4i  28460  pj11i  28570  hosubeq0i  28685  dmadjrnb  28765  nmlnop0iALT  28854  lnopeq0i  28866  elunop2  28872  lnconi  28892  lncnopbd  28896  adjbdlnb  28943  adjbd1o  28944  adjeq0  28950  rnbra  28966  pjss1coi  29022  pjss2coi  29023  pjnormssi  29027  pjssdif2i  29033  pjssdif1i  29034  dfpjop  29041  pjinvari  29050  pjin2i  29052  pjci  29059  pjcmul1i  29060  pjcmul2i  29061  strb  29117  hstrbi  29125  mdsl1i  29180  atom1d  29212  chrelat2i  29224  cvbr4i  29226  cvexchi  29228  sumdmdi  29279  dmdbr4ati  29280  dmdbr5ati  29281  dmdbr6ati  29282  dmdbr7ati  29283  cdj3i  29300  difeq  29355  iundisjf  29402  cnvoprab  29498  fpwrelmap  29508  iundisjfi  29555  xrge0tsmsbi  29786  issgon  30186  measbasedom  30265  oddpwdc  30416  eulerpartlemt  30433  ballotlem2  30550  ballotlemrinv  30595  bnj1533  30922  bnj983  31021  elmsta  31445  nepss  31599  dford5  31608  dfpo2  31645  dfon2  31697  distel  31709  elno2  31807  bdayfo  31828  fnimage  32036  altopthsn  32068  ellines  32259  rankeq1o  32278  opnrebl2  32316  df3nandALT1  32396  pm4.81ALT  32546  bj-dfbi6  32560  bj-consensus  32562  bj-falor2  32570  bj-bibibi  32571  bj-andnotim  32573  bj-ssbeq  32627  bj-ssb0  32628  bj-19.41al  32637  bj-sb56  32639  bj-eqs  32663  bj-cbvexw  32664  bj-sb  32677  bj-equs45fv  32752  bj-sbfvv  32765  bj-sb6  32767  bj-axext4  32770  bj-hbaeb2  32805  bj-hbnaeb  32807  bj-equsal  32813  bj-sbsb  32824  bj-mo3OLD  32832  bj-cleqhyp  32892  bj-csbsnlem  32898  bj-snsetex  32951  bj-snglex  32961  bj-1uplth  32995  bj-1uplex  32996  bj-2uplth  33009  bj-2uplex  33010  bj-restpw  33045  bj-restuni  33050  bj-ismooredr2  33065  bj-discrmoore  33066  bj-snmoore  33068  bj-elid  33085  bj-elid3  33087  bj-eldiag2  33092  mptsnunlem  33185  topdifinf  33197  elxp8  33219  finxp1o  33229  wl-nfnbi  33314  wl-exeq  33321  wl-aleq  33322  wl-nfeqfb  33323  wl-ax11-lem6  33367  volsupnfl  33454  cover2  33508  isbnd3  33583  cntotbnd  33595  heibor  33620  isfld2  33804  isfldidl  33867  orfa  33881  eqelb  34002  iss2  34112  prtlem16  34154  isltrn2N  35406  ismrc  37264  isnacs3  37273  rexzrexnn0  37368  eldioph4b  37375  dford3  37595  wopprc  37597  ttac  37603  pw2f1ocnv  37604  dfac11  37632  dfac21  37636  isnumbasabl  37676  isnumbasgrp  37677  dfacbasgrp  37678  aaitgo  37732  ifpbi1b  37848  rp-fakeimass  37857  rp-fakeanorass  37858  rp-fakenanass  37860  rp-isfinite5  37863  rp-isfinite6  37864  rtrclex  37924  cnvtrrel  37962  rp-imass  38065  frege54cor0a  38157  isotone1  38346  isotone2  38347  gneispace  38432  k0004lem3  38447  nanorxor  38504  nzss  38516  pm10.55  38568  pm11.57  38589  sbeqalbi  38601  pm13.192  38611  pm13.194  38613  ipo0  38653  ifr0  38654  xpexb  38658  3impexpbicom  38685  com3rgbi  38720  pm2.43bgbi  38723  pm2.43cbi  38724  sb5ALT  38731  trsbc  38750  2pm13.193  38768  ax6e2ndeq  38775  2uasbanh  38777  eelT01  38936  eel0T1  38937  uunT1  39007  zfregs2VD  39076  equncomVD  39104  trsbcVD  39113  undif3VD  39118  2pm13.193VD  39139  ax6e2eqVD  39143  ax6e2ndeqVD  39145  2uasbanhVD  39147  ax6e2ndeqALT  39167  fompt  39379  mptssid  39450  elfzfzo  39488  allbutfi  39616  uzn0bi  39689  dvnprodlem3  40163  elaa2  40451  sge00  40593  ismea  40668  elhoi  40756  ovn0  40780  ovolval4lem2  40864  confun  41106  reuan  41180  afvfv0bi  41232  ffnafv  41251  sbgoldbmb  41674  mgm2mgm  41863  isringrng  41881  nnpw2pb  42381  elsetrecs  42445  elpg  42457