Theorem impbii 181

Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)

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 180	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 9	1 |- ( ph <-> ps )

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

This theorem is referenced by:  dfbi1  185  bicom  192  biid  228  2th  231  pm5.74  236  bitri  241  notnot  283  con34b  284  notbi  287  bibi2i  305  con1b  324  con2b  325  bi2.04  351  pm5.4  352  imdi  353  pm4.8  355  pm4.81  356  orcom  377  dfor2  401  impexp  434  ancom  438  oridm  501  orbi2i  506  or12  510  pm4.45im  546  pm4.44  561  pm4.79  567  anass  631  jaob  759  jcab  834  andi  838  pm4.72  847  oibabs  852  pm4.82  895  consensus  926  rnlem  932  3jaob  1246  truan  1337  dfnot  1338  3impexp  1372  3impexpbicom  1373  cad1  1404  tbw-bijust  1469  tbw-negdf  1470  19.26  1600  sbbii  1661  19.9v  1672  equcom  1688  19.3vOLD  1705  cbvalw  1710  cbvalvwOLD  1712  alcom  1748  19.3  1787  19.9hOLD  1791  19.23hOLD  1835  equsalhwOLD  1857  19.21hOLD  1858  excomOLD  1878  19.41  1896  19.41OLD  1897  equsalOLD  1967  equsex  1969  ax12olem1  1972  ax12olem1OLD  1977  ax12olem3OLD  1979  cbval  2037  equs45f  2044  equvin  2051  sb6f  2088  dfsb2  2104  sbn  2111  sbim  2114  sb5rf  2139  sb6rf  2140  sb9  2144  mo  2276  eu2  2279  mo2  2283  exmoeu  2296  euan  2311  2mo  2332  2eu6  2339  axext4  2388  cleqh  2501  nebi  2638  r19.26  2798  ralcom3  2833  ceqsex  2950  gencbvex  2958  gencbvex2  2959  eqvinc  3023  pm13.183  3036  rr19.3v  3037  rr19.28v  3038  euxfr2  3079  reu6  3083  reu3  3084  sbnfc2  3269  sspss  3406  unineq  3551  uneqin  3552  undif3  3562  difrab  3575  un00  3623  ssdifeq0  3670  r19.2zb  3678  ralf0  3694  elpr2  3793  snidb  3800  tppreqb  3899  difsnb  3900  pwpw0  3906  sssn  3917  preq12b  3934  preqsn  3940  pwsnALT  3970  unissint  4034  uniintsn  4047  iununi  4135  intex  4316  intnex  4317  iin0  4333  axpweq  4336  nfcvb  4354  sspwb  4373  unipw  4374  opnz  4392  opth  4395  opthwiener  4418  ssopab2b  4441  pwssun  4449  elon2  4552  unexb  4668  eusvnfb  4678  eusv2nf  4680  ralxfrALT  4701  uniexb  4711  iunpw  4718  ordeleqon  4728  onintrab  4740  unon  4770  onuninsuci  4779  ordzsl  4784  onzsl  4785  opelxp  4867  opthprc  4884  relop  4982  issetid  4986  xpid11  5050  elres  5140  iss  5148  issref  5206  asymref2  5210  xpnz  5251  ssrnres  5268  dfrel2  5280  relrelss  5352  unixp0  5362  fn0  5523  funssxp  5563  f00  5587  dffo2  5616  ffoss  5666  f1o00  5669  fo00  5670  fv3  5703  dffn5  5731  dff2  5840  dff3  5841  dffo4  5844  dffo5  5845  exfo  5846  fmpt  5849  ffnfv  5853  fsn  5865  fsn2  5867  fconstfv  5913  isores1  6013  ssoprab2b  6090  eqfnov2  6136  1st2ndb  6346  reldmtpos  6446  riotaundb  6550  abianfp  6675  omopthi  6859  mapsn  7014  mapsncnv  7019  mptelixpg  7058  elixpsn  7060  ixpsnf1o  7061  bren2  7097  en0  7129  en1  7133  en1b  7134  sbthb  7187  canth2  7219  onfin2  7257  sdom1  7267  1sdom  7270  fineqv  7283  unfilem1  7330  fiint  7342  pwfi  7360  unifpw  7367  wofib  7470  sucprcreg  7523  opthreg  7529  suc11reg  7530  infeq5  7548  rankwflemb  7675  r1elss  7688  pwwf  7689  unwf  7692  uniwf  7701  rankonid  7711  rankr1id  7744  rankuni  7745  rankxplim3  7761  scott0  7766  karden  7775  isnum3  7797  oncard  7803  card1  7811  cardlim  7815  cardmin2  7841  pm54.43lem  7842  ween  7872  acnnum  7889  alephsuc2  7917  alephgeom  7919  iscard3  7930  dfac3  7958  dfac4  7959  dfac5lem3  7962  dfac5  7965  dfac2  7967  dfac8  7971  dfac9  7972  dfacacn  7977  dfac13  7978  dfac12r  7982  dfac12k  7983  kmlem2  7987  kmlem13  7998  cdainf  8028  ackbij2  8079  cflim2  8099  isfin4-2  8150  isfin4-3  8151  isf33lem  8202  compsscnv  8207  fin1a2lem6  8241  domtriom  8279  ac9  8319  ac9s  8329  fodomb  8360  brdom3  8362  brdom5  8363  brdom4  8364  brdom7disj  8365  brdom6disj  8366  iunfo  8370  sdomsdomcard  8391  gch2  8510  gch3  8511  eltsk2g  8582  grutsk  8653  grothpw  8657  ordpipq  8775  ltbtwnnq  8811  mappsrpr  8939  map2psrpr  8941  elreal2  8963  le2tri3i  9159  ltadd2i  9160  elnn0nn  10218  elnnnn0b  10220  elnnnn0c  10221  elnnz  10248  elnn0z  10250  elz2  10254  elnnz1  10263  eluz2b2  10504  elnn1uz2  10508  elioo4g  10927  eluzfz2b  11022  fzn0  11026  elfz1end  11037  fzass4  11046  fzolb  11100  fzon0  11111  elfzo0  11126  elfzo1  11128  om2uzrani  11247  nn0opthi  11518  hashkf  11575  hashprb  11623  hashf1  11661  wrdexb  11718  sqr0lem  12001  rexanuz  12104  rexuz3  12107  fsum0diag  12516  sadcp1  12922  isprm6  13064  4sqlem4  13275  mreunirn  13781  isdrs2  14351  isacs5  14553  isacs4  14554  isacs3  14555  isnsg3  14929  gicer  15018  oppgmndb  15106  oppggrpb  15109  invghm  15408  opprrngb  15692  abvn0b  16317  gzrngunit  16719  zrngunit  16720  dvdsrz  16722  zlmlmod  16759  zlmassa  16760  cygth  16807  frgpcyg  16809  tgclb  16990  iscldtop  17114  isnrm2  17376  isnrm3  17377  discmp  17415  dfcon2  17435  2ndcsb  17465  dis2ndc  17476  loclly  17503  iskgen2  17533  dfac14  17603  kqtop  17730  kqt0  17731  kqreg  17736  kqnrm  17737  hmpher  17769  hmphsymb  17771  hmph0  17780  kqhmph  17804  ist1-5lem  17805  elmptrab2  17813  isfil2  17841  filunirn  17867  isufil2  17893  hausflim  17966  isfcls  17994  alexsubALT  18035  istgp2  18074  ustbas  18210  xmetunirn  18320  dscmet  18573  dscopn  18574  isngp4  18611  zcld  18797  zlmclm  19073  iscmet2  19200  iundisj  19395  i1f1lem  19534  fta1b  20045  elply2  20068  elqaa  20192  aannenlem2  20199  wilth  20807  lgsne0  21070  2sqlem2  21101  ostth  21286  uhgra0v  21298  wrdumgra  21304  usgra0v  21344  uvtx01vtx  21454  istrl2  21491  isspthonpth  21537  nmlno0lem  22247  isblo3i  22255  blocni  22259  hvsubeq0i  22518  hvaddcani  22520  bcseqi  22575  isch3  22697  norm1exi  22705  hhsssh  22722  shslubi  22840  dfch2  22862  pjoc1i  22886  pjchi  22887  shs00i  22905  chsscon3i  22916  chlejb1i  22931  chj00i  22942  shjshseli  22948  h1de2ctlem  23010  spanunsni  23034  cmcmi  23047  cmbr3i  23055  cmbr4i  23056  pj11i  23166  hosubeq0i  23282  dmadjrnb  23362  nmlnop0iALT  23451  lnopeq0i  23463  elunop2  23469  lnconi  23489  lncnopbd  23493  adjbdlnb  23540  adjbd1o  23541  adjeq0  23547  rnbra  23563  pjss1coi  23619  pjss2coi  23620  pjnormssi  23624  pjssdif2i  23630  pjssdif1i  23631  dfpjop  23638  pjinvari  23647  pjin2i  23649  pjci  23656  pjcmul1i  23657  pjcmul2i  23658  strb  23714  hstrbi  23722  mdsl1i  23777  atom1d  23809  chrelat2i  23821  cvbr4i  23823  cvexchi  23825  sumdmdi  23876  dmdbr4ati  23877  dmdbr5ati  23878  dmdbr6ati  23879  dmdbr7ati  23880  cdj3i  23897  difeq  23951  iundisjf  23982  iundisjfi  24105  xrge0tsmsbi  24177  issgon  24459  measbasedom  24509  ballotlem2  24699  ballotlemrinv  24744  nepss  25128  fprod0diag  25263  dfpo2  25326  dfon2  25362  distel  25374  elno2  25522  bdayfo  25543  elfix  25657  dffix2  25659  fnimage  25682  altopthsn  25710  mptelee  25738  ellines  25990  rankeq1o  26016  df3nandALT1  26050  wl-pm5.74lem  26131  volsupnfl  26150  opnrebl2  26214  locfindis  26275  cover2  26305  isbnd3  26383  cntotbnd  26395  heibor  26420  isfld2  26505  isfldidl  26568  prtlem16  26608  funsnfsup  26633  ismrc  26645  isnacs3  26654  rexzrexnn0  26754  eldioph4b  26762  dford3  26989  wopprc  26991  ttac  26997  pw2f1ocnv  26998  dfac11  27028  dfac21  27032  isnumbasabl  27139  isnumbasgrp  27140  dfacbasgrp  27141  aaitgo  27235  pmtrfb  27274  pm10.55  27432  pm11.57  27456  sbeqalbi  27468  pm13.192  27478  pm13.194  27480  ipo0  27519  ifr0  27520  xpexb  27525  reuan  27825  afvfv0bi  27883  ffnafv  27902  fzo1fzo0n0  27988  usg2spthonot1  28087  frgra0v  28097  com3rgbi  28308  pm2.43bgbi  28311  pm2.43cbi  28312  sb5ALT  28320  trsbc  28336  2pm13.193  28350  a9e2ndeq  28357  2uasbanh  28359  eelT01  28527  eel0T1  28528  uunT1  28601  zfregs2VD  28662  equncomVD  28689  trsbcVD  28698  undif3VD  28703  2pm13.193VD  28724  a9e2eqVD  28728  a9e2ndeqVD  28730  2uasbanhVD  28732  a9e2ndeqALT  28753  bnj1533  28929  bnj983  29028  alcomwAUX7  29150  ax12olem3aAUX7  29163  equsalNEW7  29193  cbvalwwAUX7  29223  equvinNEW7  29233  sbnNEW7  29266  sbimNEW7  29269  sb5rfNEW7  29292  sb6rfNEW7  29293  sb8wAUX7  29294  equs45fNEW7  29322  sb6fNEW7  29334  dfsb2NEW7  29339  alcomw9bAUX7  29361  alcomOLD7  29365  excomOLD7  29378  cbvalOLD7  29409  nfsb4tw2AUXOLD7  29430  sbcomOLD7  29439  sb8OLD7  29440  sb9iOLD7  29442  sb9OLD7  29443  isltrn2N  30602

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178