Theorem impbii 188

Description: Infer an equivalence from an implication and its converse. (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		bi3 187	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 9	1 |- ( ph <-> ps )

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

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 185

This theorem is referenced by:  dfbi1  192  bicom  200  biid  236  2th  239  pm5.74  244  bitri  249  notnot  291  con34b  292  notbi  295  bibi2i  313  con1b  333  con2b  334  bi2.04  361  pm5.4  362  imdi  363  pm4.8  365  pm4.81  366  orcom  387  dfor2  411  impexp  446  ancom  450  oridm  514  orbi2i  519  or12  523  pm4.45im  562  pm4.44  577  pm4.79  583  anass  649  jaob  781  jcab  858  andi  862  pm4.72  871  oibabs  876  pm4.82  919  consensus  950  rnlem  956  cases2  963  3jaob  1281  truanOLD  1388  dfnotOLD  1390  cad1  1441  tbw-bijust  1506  tbw-negdf  1507  19.26  1648  19.35  1655  sbbii  1709  19.9v  1719  equcom  1734  equvin  1744  cbvalw  1748  alcom  1785  19.3  1824  19.41  1908  cbval  1978  equsex  1995  aecom  2008  equvinOLD  2047  equs45f  2048  dfsb2  2071  sb6f  2083  sbnOLD  2090  sbim  2094  sb5rfOLD  2128  sb6rfOLD  2130  sb9OLD  2136  sb6  2140  mo2v  2267  mo2vOLD  2268  mo2vOLDOLD  2269  exmoeu  2296  exmoeuOLD  2297  mo3  2305  mo3OLD  2306  moOLD  2312  eu2OLD  2314  mo2OLD  2321  moanim  2337  euan  2338  euanOLD  2339  2mo  2367  2moOLD  2368  2moOLDOLD  2369  2eu6  2378  2eu6OLD  2379  axext4  2433  eqcom  2460  cleqhOLD  2567  nebi  2758  r19.26  2945  ralcom3  2982  ceqsex  3104  gencbvex  3112  gencbvex2  3113  eqvinc  3183  pm13.183  3197  rr19.3v  3198  rr19.28v  3199  euxfr2  3241  reu6  3245  reu3  3246  sspss  3553  unineq  3698  uneqin  3699  undif3  3709  difrab  3722  sbnfc2  3804  un00  3812  ssdifeq0  3859  r19.2zb  3868  ralf0  3884  elpr2  3994  snidb  4002  rabsnifsb  4041  tppreqb  4112  difsnb  4113  pwpw0  4119  sssn  4129  preq12b  4146  preqsn  4153  pwsnALT  4184  unissint  4250  uniintsn  4263  iununi  4353  intex  4546  intnex  4547  iin0  4564  axpweq  4567  eusvnfb  4586  eusv2nf  4588  ralxfrALT  4609  nfcvb  4620  sspwb  4639  unipw  4640  opnz  4661  opth  4664  opthwiener  4691  ssopab2b  4713  pwssun  4725  elon2  4828  opelxp  4967  opthprc  4984  relop  5088  issetid  5092  xpid11  5159  elres  5243  iss  5252  restidsing  5260  issref  5309  asymref2  5313  xpnz  5355  xpdifid  5364  ssrnres  5374  dfrel2  5386  relrelss  5459  unixp0  5469  fn0  5628  funssxp  5669  f00  5691  f0bi  5692  dffo2  5722  f1o00  5771  fo00  5772  fv3  5802  dffn5  5836  dff2  5954  dff3  5955  dffo4  5958  dffo5  5959  exfo  5960  fmpt  5963  ffnfv  5968  fsn  5980  fsn2  5982  fnsnb  5997  fconstfv  6039  isores1  6124  ssoprab2b  6242  eqfnov2  6297  unexb  6480  uniexb  6486  iunpw  6490  ordeleqon  6500  onintrab  6512  unon  6542  onuninsuci  6551  ordzsl  6556  onzsl  6557  ffoss  6638  1st2ndb  6714  suppssov1  6821  suppssfv  6825  reldmtpos  6853  omopthi  7196  mapsn  7354  mapsncnv  7359  mptelixpg  7400  elixpsn  7402  ixpsnf1o  7403  bren2  7440  en0  7472  en1  7476  en1b  7477  sbthb  7532  canth2  7564  onfin2  7603  sdom1  7613  1sdom  7616  fineqv  7629  unfilem1  7677  fiint  7689  pwfi  7707  unifpw  7715  wofib  7860  sucprcreg  7915  sucprcregOLD  7916  opthreg  7925  suc11reg  7926  infeq5  7944  rankwflemb  8101  r1elss  8114  pwwf  8115  unwf  8118  uniwf  8127  rankonid  8137  rankr1id  8170  rankuni  8171  rankxplim3  8189  scott0  8194  karden  8203  isnum3  8225  oncard  8231  card1  8239  cardlim  8243  cardmin2  8269  pm54.43lem  8270  ween  8306  acnnum  8323  alephsuc2  8351  alephgeom  8353  iscard3  8364  dfac3  8392  dfac4  8393  dfac5lem3  8396  dfac5  8399  dfac2  8401  dfac8  8405  dfac9  8406  dfacacn  8411  dfac13  8412  dfac12r  8416  dfac12k  8417  kmlem2  8421  kmlem13  8432  cdainf  8462  ackbij2  8513  cflim2  8533  isfin4-2  8584  isfin4-3  8585  isf33lem  8636  compsscnv  8641  fin1a2lem6  8675  domtriom  8713  ac9  8753  ac9s  8763  fodomb  8794  brdom3  8796  brdom5  8797  brdom4  8798  brdom7disj  8799  brdom6disj  8800  iunfo  8804  sdomsdomcard  8825  gch2  8943  gch3  8944  eltsk2g  9019  grutsk  9090  grothpw  9094  ordpipq  9212  ltbtwnnq  9248  mappsrpr  9376  map2psrpr  9378  elreal2  9400  le2tri3i  9605  ltadd2i  9606  elnn0nn  10723  elnnnn0b  10725  elnnnn0c  10726  elnnz  10757  elnn0z  10760  elz2  10764  elnnz1  10773  eluz2b2  11028  elnn1uz2  11032  elioo4g  11457  eluzfz2b  11561  fzn0  11565  elfz1end  11580  fzass4  11597  nn0fz0  11626  elfz1b  11628  fzolb  11659  fzon0  11670  elfzo0  11688  fzo1fzo0n0  11689  elfzo0z  11690  elfzo1  11696  om2uzrani  11876  nn0opthi  12149  hashkf  12206  hashprb  12259  hashf1  12312  iswrdbi  12343  wrdexb  12347  0wrd0  12355  sqr0lem  12832  rexanuz  12935  rexuz3  12938  fsum0diag  13346  sadcp1  13753  isprm6  13897  4sqlem4  14115  mreunirn  14641  isdrs2  15211  isacs5  15444  isacs4  15445  isacs3  15446  isnsg3  15817  gicer  15906  oppgmndb  15972  oppggrpb  15975  pmtrfb  16073  invghm  16422  opprrngb  16830  abvn0b  17480  funsnfsupOLD  17777  gzrngunit  17987  dvdsrzring  18010  dvdsrz  18011  zringunit  18023  zrngunit  18024  zlmlmod  18063  zlmassa  18064  cygth  18113  frgpcyg  18115  tgclb  18691  iscldtop  18815  isnrm2  19078  isnrm3  19079  discmp  19117  dfcon2  19139  2ndcsb  19169  dis2ndc  19180  loclly  19207  iskgen2  19237  dfac14  19307  kqtop  19434  kqt0  19435  kqreg  19440  kqnrm  19441  hmpher  19473  hmphsymb  19475  hmph0  19484  kqhmph  19508  ist1-5lem  19509  elmptrab2  19517  isfil2  19545  filunirn  19571  isufil2  19597  hausflim  19670  isfcls  19698  alexsubALT  19739  istgp2  19778  ustbas  19918  xmetunirn  20028  dscmet  20281  dscopn  20282  isngp4  20319  zcld  20506  zlmclm  20783  iscmet2  20921  iundisj  21145  i1f1lem  21283  fta1b  21757  elply2  21780  elqaa  21904  aannenlem2  21911  wilth  22525  lgsne0  22788  2sqlem2  22819  ostth  23004  mptelee  23276  uhgra0v  23379  wrdumgra  23385  usgra0v  23425  uvtx01vtx  23535  istrl2  23572  isspthonpth  23618  nmlno0lem  24328  isblo3i  24336  blocni  24340  hvsubeq0i  24600  hvaddcani  24602  bcseqi  24657  isch3  24779  norm1exi  24788  hhsssh  24805  shslubi  24923  dfch2  24945  pjoc1i  24969  pjchi  24970  shs00i  24988  chsscon3i  24999  chlejb1i  25014  chj00i  25025  shjshseli  25031  h1de2ctlem  25093  spanunsni  25117  cmcmi  25130  cmbr3i  25138  cmbr4i  25139  pj11i  25249  hosubeq0i  25365  dmadjrnb  25445  nmlnop0iALT  25534  lnopeq0i  25546  elunop2  25552  lnconi  25572  lncnopbd  25576  adjbdlnb  25623  adjbd1o  25624  adjeq0  25630  rnbra  25646  pjss1coi  25702  pjss2coi  25703  pjnormssi  25707  pjssdif2i  25713  pjssdif1i  25714  dfpjop  25721  pjinvari  25730  pjin2i  25732  pjci  25739  pjcmul1i  25740  pjcmul2i  25741  strb  25797  hstrbi  25805  mdsl1i  25860  atom1d  25892  chrelat2i  25904  cvbr4i  25906  cvexchi  25908  sumdmdi  25959  dmdbr4ati  25960  dmdbr5ati  25961  dmdbr6ati  25962  dmdbr7ati  25963  cdj3i  25980  difeq  26034  iundisjf  26065  cnvoprab  26157  fpwrelmap  26167  iundisjfi  26214  xrge0tsmsbi  26388  issgon  26700  measbasedom  26750  oddpwdc  26871  eulerpartlemt  26888  ballotlem2  27005  ballotlemrinv  27050  nepss  27508  fprod0diag  27631  dfpo2  27699  dfon2  27739  distel  27751  elno2  27929  bdayfo  27950  fnimage  28094  altopthsn  28126  ellines  28317  rankeq1o  28343  df3nandALT1  28377  wl-nfnbi  28493  wl-exeq  28501  wl-aleq  28502  wl-nfeqfb  28504  wl-ax11-lem6  28544  volsupnfl  28574  dvtanlem  28579  opnrebl2  28654  locfindis  28715  cover2  28745  isbnd3  28821  cntotbnd  28833  heibor  28858  isfld2  28943  isfldidl  29006  orfa  29020  prtlem16  29152  ismrc  29175  isnacs3  29184  rexzrexnn0  29280  eldioph4b  29288  dford3  29515  wopprc  29517  ttac  29523  pw2f1ocnv  29524  dfac11  29553  dfac21  29557  isnumbasabl  29600  isnumbasgrp  29601  dfacbasgrp  29602  aaitgo  29657  pm10.55  29759  pm11.57  29780  sbeqalbi  29792  pm13.192  29802  pm13.194  29804  ipo0  29843  ifr0  29844  xpexb  29848  reuan  30142  afvfv0bi  30196  ffnafv  30215  eldmeldmressn  30278  f1oexbi  30294  wlkcpr  30428  usg2spthonot1  30547  eclclwwlkn1  30644  clwlknclwlkdifs  30716  frgra0v  30723  isnzr2hash  30912  3impexp  31455  3impexpbicom  31456  com3rgbi  31519  pm2.43bgbi  31522  pm2.43cbi  31523  sb5ALT  31530  trsbc  31547  2pm13.193  31561  ax6e2ndeq  31568  2uasbanh  31570  eelT01  31739  eel0T1  31740  uunT1  31813  zfregs2VD  31877  equncomVD  31904  trsbcVD  31913  undif3VD  31918  2pm13.193VD  31939  ax6e2eqVD  31943  ax6e2ndeqVD  31945  2uasbanhVD  31947  ax6e2ndeqALT  31967  bnj1533  32145  bnj983  32244  bj-dfbi6  32379  bj-dfif5ALT  32386  bj-consensus  32399  bj-falor2  32411  bj-bibibi  32412  bj-andnotim  32414  bj-cbvalv  32532  bj-equsexv  32548  bj-equs45fv  32566  bj-sb6  32585  bj-axext4  32590  bj-cleqh  32593  bj-hbaeb  32626  bj-hbnaeb  32627  bj-equsal  32634  bj-dfcleq  32701  bj-csbsnlem  32705  bj-snsetex  32756  bj-snglex  32766  bj-1uplth  32800  bj-1uplex  32801  bj-2uplth  32814  bj-2uplex  32815  bj-elid  32826  isltrn2N  34070