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  861  andi  865  pm4.72  874  oibabs  879  pm4.82  926  consensus  957  rnlemOLD  963  cases2  970  cases2OLD  971  3jaob  1290  truanOLD  1397  dfnotOLD  1399  cad1  1450  tbw-bijust  1515  tbw-negdf  1516  19.26  1657  19.35  1664  sbbii  1718  19.9v  1728  equcom  1743  equvin  1753  cbvalw  1757  alcom  1794  19.3  1836  19.41  1920  19.21v  1930  19.23v  1932  cbval  1994  equsex  2011  aecom  2024  equvinOLD  2063  equs45f  2064  dfsb2  2087  sb6f  2099  sbnOLD  2106  sbim  2110  sb5rfOLD  2144  sb6rfOLD  2146  sb9OLD  2152  sb6  2155  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  exmoeu  2311  exmoeuOLD  2312  mo3  2320  mo3OLD  2321  moOLD  2327  eu2OLD  2329  mo2OLD  2336  moanim  2352  euan  2353  euanOLD  2354  2mo  2382  2moOLD  2383  2moOLDOLD  2384  2eu6  2393  2eu6OLD  2394  axext4  2449  eqcom  2476  cleqhOLD  2583  nebi  2777  r19.26  2989  ralcom3  3027  ceqsex  3149  gencbvex  3157  gencbvex2  3158  eqvinc  3230  pm13.183  3244  rr19.3v  3245  rr19.28v  3246  euxfr2  3288  reu6  3292  reu3  3293  sspss  3603  unineq  3748  uneqin  3749  undif3  3759  difrab  3772  sbnfc2  3854  un00  3862  ssdifeq0  3909  r19.2zb  3918  ralf0  3934  elpr2  4046  snidb  4054  rabsnifsb  4095  tppreqb  4168  difsnb  4169  pwpw0  4175  sssn  4185  preq12b  4202  preqsn  4209  pwsnALT  4240  unissint  4306  uniintsn  4319  iununi  4410  intex  4603  intnex  4604  iin0  4621  axpweq  4624  eusvnfb  4643  eusv2nf  4645  ralxfrALT  4666  nfcvb  4677  sspwb  4696  unipw  4697  opnz  4718  opth  4721  opthwiener  4749  ssopab2b  4774  pwssun  4786  elon2  4889  opelxp  5028  opthprc  5046  relop  5151  issetid  5155  xpid11  5222  elres  5307  eldmeldmressn  5312  iss  5319  restidsing  5328  issref  5378  asymref2  5382  xpnz  5424  xpdifid  5433  ssrnres  5443  dfrel2  5455  relrelss  5529  unixp0  5539  fn0  5698  funssxp  5742  f00  5765  f0bi  5766  dffo2  5797  f1o00  5846  fo00  5847  fv3  5877  dffn5  5911  dff2  6031  dff3  6032  dffo4  6035  dffo5  6036  exfo  6037  fmpt  6040  ffnfv  6045  fsn  6057  fsn2  6059  fnsnb  6078  fconstfv  6121  isores1  6216  ssoprab2b  6336  eqfnov2  6391  unexb  6582  uniexb  6588  iunpw  6592  ordeleqon  6602  onintrab  6614  unon  6644  onuninsuci  6653  ordzsl  6658  onzsl  6659  f1oexbi  6731  ffoss  6742  1st2ndb  6819  suppssov1  6929  suppssfv  6933  reldmtpos  6960  omopthi  7303  mapsn  7457  mapsncnv  7462  mptelixpg  7503  elixpsn  7505  ixpsnf1o  7506  bren2  7543  en0  7575  en1  7579  en1b  7580  sbthb  7635  canth2  7667  onfin2  7706  sdom1  7716  1sdom  7719  fineqv  7732  unfilem1  7780  fiint  7793  pwfi  7811  unifpw  7819  wofib  7966  sucprcreg  8021  sucprcregOLD  8022  opthreg  8031  suc11reg  8032  infeq5  8050  rankwflemb  8207  r1elss  8220  pwwf  8221  unwf  8224  uniwf  8233  rankonid  8243  rankr1id  8276  rankuni  8277  rankxplim3  8295  scott0  8300  karden  8309  isnum3  8331  oncard  8337  card1  8345  cardlim  8349  cardmin2  8375  pm54.43lem  8376  ween  8412  acnnum  8429  alephsuc2  8457  alephgeom  8459  iscard3  8470  dfac3  8498  dfac4  8499  dfac5lem3  8502  dfac5  8505  dfac2  8507  dfac8  8511  dfac9  8512  dfacacn  8517  dfac13  8518  dfac12r  8522  dfac12k  8523  kmlem2  8527  kmlem13  8538  cdainf  8568  ackbij2  8619  cflim2  8639  isfin4-2  8690  isfin4-3  8691  isf33lem  8742  compsscnv  8747  fin1a2lem6  8781  domtriom  8819  ac9  8859  ac9s  8869  fodomb  8900  brdom3  8902  brdom5  8903  brdom4  8904  brdom7disj  8905  brdom6disj  8906  iunfo  8910  sdomsdomcard  8931  gch2  9049  gch3  9050  eltsk2g  9125  grutsk  9196  grothpw  9200  ordpipq  9316  ltbtwnnq  9352  mappsrpr  9481  map2psrpr  9483  elreal2  9505  le2tri3i  9710  ltadd2i  9711  elnn0nn  10834  elnnnn0b  10836  elnnnn0c  10837  elnnz  10870  elnn0z  10873  elz2  10877  elnnz1  10886  eluz2b2  11150  elnn1uz2  11154  elioo4g  11581  eluzfz2b  11691  fzn0  11696  elfz1end  11711  fzass4  11717  elfz1b  11744  nn0fz0  11769  fzolb  11798  fzon0  11809  elfzo0  11827  fzo1fzo0n0  11828  elfzo0z  11829  elfzo1  11835  om2uzrani  12026  nn0opthi  12312  hashkf  12369  hashprb  12424  hashf1  12466  iswrdbi  12514  wrdexb  12518  0wrd0  12526  sqr0lem  13031  rexanuz  13134  rexuz3  13137  fsum0diag  13548  sadcp1  13957  isprm6  14102  4sqlem4  14322  mreunirn  14849  isdrs2  15419  isacs5  15652  isacs4  15653  isacs3  15654  isnsg3  16027  gicer  16116  oppgmndb  16182  oppggrpb  16185  pmtrfb  16283  invghm  16632  opprrngb  17062  abvn0b  17719  funsnfsupOLD  18024  gzrngunit  18248  dvdsrzring  18271  dvdsrz  18272  zringunit  18284  zrngunit  18285  zlmlmod  18324  zlmassa  18325  cygth  18374  frgpcyg  18376  tgclb  19235  iscldtop  19359  isnrm2  19622  isnrm3  19623  discmp  19661  dfcon2  19683  2ndcsb  19713  dis2ndc  19724  loclly  19751  iskgen2  19781  dfac14  19851  kqtop  19978  kqt0  19979  kqreg  19984  kqnrm  19985  hmpher  20017  hmphsymb  20019  hmph0  20028  kqhmph  20052  ist1-5lem  20053  elmptrab2  20061  isfil2  20089  filunirn  20115  isufil2  20141  hausflim  20214  isfcls  20242  alexsubALT  20283  istgp2  20322  ustbas  20462  xmetunirn  20572  dscmet  20825  dscopn  20826  isngp4  20863  zcld  21050  zlmclm  21327  iscmet2  21465  iundisj  21690  i1f1lem  21828  fta1b  22302  elply2  22325  elqaa  22449  aannenlem2  22456  wilth  23070  lgsne0  23333  2sqlem2  23364  ostth  23549  mptelee  23871  uhgra0v  23983  wrdumgra  23989  usgra0v  24044  uvtx01vtx  24165  wlkcpr  24202  istrl2  24213  isspthonpth  24259  eclclwwlkn1  24505  usg2spthonot1  24563  clwlknclwlkdifs  24633  frgra0v  24666  nmlno0lem  25381  isblo3i  25389  blocni  25393  hvsubeq0i  25653  hvaddcani  25655  bcseqi  25710  isch3  25832  norm1exi  25841  hhsssh  25858  shslubi  25976  dfch2  25998  pjoc1i  26022  pjchi  26023  shs00i  26041  chsscon3i  26052  chlejb1i  26067  chj00i  26078  shjshseli  26084  h1de2ctlem  26146  spanunsni  26170  cmcmi  26183  cmbr3i  26191  cmbr4i  26192  pj11i  26302  hosubeq0i  26418  dmadjrnb  26498  nmlnop0iALT  26587  lnopeq0i  26599  elunop2  26605  lnconi  26625  lncnopbd  26629  adjbdlnb  26676  adjbd1o  26677  adjeq0  26683  rnbra  26699  pjss1coi  26755  pjss2coi  26756  pjnormssi  26760  pjssdif2i  26766  pjssdif1i  26767  dfpjop  26774  pjinvari  26783  pjin2i  26785  pjci  26792  pjcmul1i  26793  pjcmul2i  26794  strb  26850  hstrbi  26858  mdsl1i  26913  atom1d  26945  chrelat2i  26957  cvbr4i  26959  cvexchi  26961  sumdmdi  27012  dmdbr4ati  27013  dmdbr5ati  27014  dmdbr6ati  27015  dmdbr7ati  27016  cdj3i  27033  difeq  27087  iundisjf  27118  cnvoprab  27215  fpwrelmap  27225  iundisjfi  27266  xrge0tsmsbi  27436  issgon  27760  measbasedom  27810  oddpwdc  27930  eulerpartlemt  27947  ballotlem2  28064  ballotlemrinv  28109  nepss  28567  fprod0diag  28690  dfpo2  28758  dfon2  28798  distel  28810  elno2  28988  bdayfo  29009  fnimage  29153  altopthsn  29185  ellines  29376  rankeq1o  29402  df3nandALT1  29436  wl-nfnbi  29553  wl-exeq  29561  wl-aleq  29562  wl-nfeqfb  29564  wl-ax11-lem6  29604  volsupnfl  29634  dvtanlem  29639  opnrebl2  29714  locfindis  29775  cover2  29805  isbnd3  29881  cntotbnd  29893  heibor  29918  isfld2  30003  isfldidl  30066  orfa  30080  prtlem16  30212  ismrc  30235  isnacs3  30244  rexzrexnn0  30339  eldioph4b  30347  dford3  30574  wopprc  30576  ttac  30582  pw2f1ocnv  30583  dfac11  30612  dfac21  30616  isnumbasabl  30659  isnumbasgrp  30660  dfacbasgrp  30661  aaitgo  30716  nzss  30822  pm10.55  30852  pm11.57  30873  sbeqalbi  30885  pm13.192  30895  pm13.194  30897  ipo0  30936  ifr0  30937  xpexb  30941  elfzfzo  31035  reuan  31652  afvfv0bi  31704  ffnafv  31723  residfi  31783  iopmapxp  31960  mgm2mgm  31977  isnzr2hash  32027  3impexp  32299  3impexpbicom  32300  com3rgbi  32363  pm2.43bgbi  32366  pm2.43cbi  32367  sb5ALT  32374  trsbc  32391  2pm13.193  32405  ax6e2ndeq  32412  2uasbanh  32414  eelT01  32583  eel0T1  32584  uunT1  32657  zfregs2VD  32721  equncomVD  32748  trsbcVD  32757  undif3VD  32762  2pm13.193VD  32783  ax6e2eqVD  32787  ax6e2ndeqVD  32789  2uasbanhVD  32791  ax6e2ndeqALT  32811  bnj1533  32989  bnj983  33088  bj-dfbi6  33223  bj-dfif5ALT  33230  bj-consensus  33243  bj-falor2  33255  bj-bibibi  33256  bj-andnotim  33258  bj-cbvalv  33378  bj-equsexv  33394  bj-equs45fv  33412  bj-sb6  33431  bj-axext4  33436  bj-cleqh  33439  bj-hbaeb2  33472  bj-hbnaeb  33474  bj-equsal  33480  bj-dfcleq  33547  bj-csbsnlem  33551  bj-snsetex  33602  bj-snglex  33612  bj-1uplth  33646  bj-1uplex  33647  bj-2uplth  33660  bj-2uplex  33661  bj-elid  33672  isltrn2N  34916  cnvtrrel  36792  rp-imass  36796  bj-frege54cor0a  36872