Theorem impbii 188

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 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  1280  truanOLD  1387  dfnotOLD  1389  cad1  1440  tbw-bijust  1505  tbw-negdf  1506  19.26  1647  19.35  1654  sbbii  1707  19.9v  1717  equcom  1732  equvin  1742  cbvalw  1746  alcom  1783  19.3  1821  19.41  1898  cbval  1969  equsex  1986  aecom  1998  equvinOLD  2040  equs45f  2041  dfsb2  2064  sb6f  2076  sbnOLD  2083  sbim  2087  sb5rfOLD  2121  sb6rfOLD  2123  sb9OLD  2129  sb6  2133  mo2v  2259  mo2vOLD  2260  exmoeu  2287  exmoeuOLD  2288  mo3  2296  mo3OLD  2297  moOLD  2303  eu2OLD  2305  mo2OLD  2312  moanim  2328  euan  2329  euanOLD  2330  2mo  2357  2moOLD  2358  2moOLDOLD  2359  2eu6  2367  2eu6OLD  2368  axext4  2422  cleqh  2535  nebi  2677  r19.26  2844  ralcom3  2881  ceqsex  3003  gencbvex  3011  gencbvex2  3012  eqvinc  3081  pm13.183  3095  rr19.3v  3096  rr19.28v  3097  euxfr2  3139  reu6  3143  reu3  3144  sspss  3450  unineq  3595  uneqin  3596  undif3  3606  difrab  3619  sbnfc2  3701  un00  3709  ssdifeq0  3756  r19.2zb  3765  ralf0  3781  elpr2  3891  snidb  3899  rabsnifsb  3938  tppreqb  4009  difsnb  4010  pwpw0  4016  sssn  4026  preq12b  4043  preqsn  4050  pwsnALT  4081  unissint  4147  uniintsn  4160  iununi  4250  intex  4443  intnex  4444  iin0  4461  axpweq  4464  eusvnfb  4483  eusv2nf  4485  ralxfrALT  4506  nfcvb  4517  sspwb  4536  unipw  4537  opnz  4558  opth  4561  opthwiener  4588  ssopab2b  4610  pwssun  4622  elon2  4725  opelxp  4864  opthprc  4881  relop  4985  issetid  4989  xpid11  5056  elres  5140  iss  5149  restidsing  5157  issref  5206  asymref2  5210  xpnz  5252  xpdifid  5261  ssrnres  5271  dfrel2  5283  relrelss  5356  unixp0  5366  fn0  5525  funssxp  5566  f00  5588  f0bi  5589  dffo2  5619  f1o00  5668  fo00  5669  fv3  5698  dffn5  5732  dff2  5850  dff3  5851  dffo4  5854  dffo5  5855  exfo  5856  fmpt  5859  ffnfv  5864  fsn  5876  fsn2  5878  fnsnb  5893  fconstfv  5935  isores1  6020  ssoprab2b  6138  eqfnov2  6192  unexb  6375  uniexb  6381  iunpw  6385  ordeleqon  6395  onintrab  6407  unon  6437  onuninsuci  6446  ordzsl  6451  onzsl  6452  ffoss  6533  1st2ndb  6609  suppssov1  6716  suppssfv  6720  reldmtpos  6748  omopthi  7088  mapsn  7246  mapsncnv  7251  mptelixpg  7292  elixpsn  7294  ixpsnf1o  7295  bren2  7332  en0  7364  en1  7368  en1b  7369  sbthb  7424  canth2  7456  onfin2  7494  sdom1  7504  1sdom  7507  fineqv  7520  unfilem1  7568  fiint  7580  pwfi  7598  unifpw  7606  wofib  7751  sucprcreg  7806  sucprcregOLD  7807  opthreg  7816  suc11reg  7817  infeq5  7835  rankwflemb  7992  r1elss  8005  pwwf  8006  unwf  8009  uniwf  8018  rankonid  8028  rankr1id  8061  rankuni  8062  rankxplim3  8080  scott0  8085  karden  8094  isnum3  8116  oncard  8122  card1  8130  cardlim  8134  cardmin2  8160  pm54.43lem  8161  ween  8197  acnnum  8214  alephsuc2  8242  alephgeom  8244  iscard3  8255  dfac3  8283  dfac4  8284  dfac5lem3  8287  dfac5  8290  dfac2  8292  dfac8  8296  dfac9  8297  dfacacn  8302  dfac13  8303  dfac12r  8307  dfac12k  8308  kmlem2  8312  kmlem13  8323  cdainf  8353  ackbij2  8404  cflim2  8424  isfin4-2  8475  isfin4-3  8476  isf33lem  8527  compsscnv  8532  fin1a2lem6  8566  domtriom  8604  ac9  8644  ac9s  8654  fodomb  8685  brdom3  8687  brdom5  8688  brdom4  8689  brdom7disj  8690  brdom6disj  8691  iunfo  8695  sdomsdomcard  8716  gch2  8834  gch3  8835  eltsk2g  8910  grutsk  8981  grothpw  8985  ordpipq  9103  ltbtwnnq  9139  mappsrpr  9267  map2psrpr  9269  elreal2  9291  le2tri3i  9496  ltadd2i  9497  elnn0nn  10614  elnnnn0b  10616  elnnnn0c  10617  elnnz  10648  elnn0z  10651  elz2  10655  elnnz1  10664  eluz2b2  10919  elnn1uz2  10923  elioo4g  11348  eluzfz2b  11452  fzn0  11456  elfz1end  11471  fzass4  11488  nn0fz0  11517  elfz1b  11519  fzolb  11550  fzon0  11561  elfzo0  11579  fzo1fzo0n0  11580  elfzo0z  11581  elfzo1  11587  om2uzrani  11767  nn0opthi  12040  hashkf  12097  hashprb  12149  hashf1  12202  iswrdbi  12233  wrdexb  12237  0wrd0  12245  sqr0lem  12722  rexanuz  12825  rexuz3  12828  fsum0diag  13236  sadcp1  13643  isprm6  13787  4sqlem4  14005  mreunirn  14531  isdrs2  15101  isacs5  15334  isacs4  15335  isacs3  15336  isnsg3  15706  gicer  15795  oppgmndb  15861  oppggrpb  15864  pmtrfb  15962  invghm  16309  opprrngb  16712  abvn0b  17351  funsnfsupOLD  17645  gzrngunit  17853  dvdsrzring  17876  dvdsrz  17877  zringunit  17889  zrngunit  17890  zlmlmod  17929  zlmassa  17930  cygth  17979  frgpcyg  17981  tgclb  18550  iscldtop  18674  isnrm2  18937  isnrm3  18938  discmp  18976  dfcon2  18998  2ndcsb  19028  dis2ndc  19039  loclly  19066  iskgen2  19096  dfac14  19166  kqtop  19293  kqt0  19294  kqreg  19299  kqnrm  19300  hmpher  19332  hmphsymb  19334  hmph0  19343  kqhmph  19367  ist1-5lem  19368  elmptrab2  19376  isfil2  19404  filunirn  19430  isufil2  19456  hausflim  19529  isfcls  19557  alexsubALT  19598  istgp2  19637  ustbas  19777  xmetunirn  19887  dscmet  20140  dscopn  20141  isngp4  20178  zcld  20365  zlmclm  20642  iscmet2  20780  iundisj  21004  i1f1lem  21142  fta1b  21616  elply2  21639  elqaa  21763  aannenlem2  21770  wilth  22384  lgsne0  22647  2sqlem2  22678  ostth  22863  mptelee  23092  uhgra0v  23195  wrdumgra  23201  usgra0v  23241  uvtx01vtx  23351  istrl2  23388  isspthonpth  23434  nmlno0lem  24144  isblo3i  24152  blocni  24156  hvsubeq0i  24416  hvaddcani  24418  bcseqi  24473  isch3  24595  norm1exi  24604  hhsssh  24621  shslubi  24739  dfch2  24761  pjoc1i  24785  pjchi  24786  shs00i  24804  chsscon3i  24815  chlejb1i  24830  chj00i  24841  shjshseli  24847  h1de2ctlem  24909  spanunsni  24933  cmcmi  24946  cmbr3i  24954  cmbr4i  24955  pj11i  25065  hosubeq0i  25181  dmadjrnb  25261  nmlnop0iALT  25350  lnopeq0i  25362  elunop2  25368  lnconi  25388  lncnopbd  25392  adjbdlnb  25439  adjbd1o  25440  adjeq0  25446  rnbra  25462  pjss1coi  25518  pjss2coi  25519  pjnormssi  25523  pjssdif2i  25529  pjssdif1i  25530  dfpjop  25537  pjinvari  25546  pjin2i  25548  pjci  25555  pjcmul1i  25556  pjcmul2i  25557  strb  25613  hstrbi  25621  mdsl1i  25676  atom1d  25708  chrelat2i  25720  cvbr4i  25722  cvexchi  25724  sumdmdi  25775  dmdbr4ati  25776  dmdbr5ati  25777  dmdbr6ati  25778  dmdbr7ati  25779  cdj3i  25796  difeq  25850  iundisjf  25882  cnvoprab  25974  fpwrelmap  25984  iundisjfi  26031  xrge0tsmsbi  26205  issgon  26518  measbasedom  26568  oddpwdc  26689  eulerpartlemt  26706  ballotlem2  26823  ballotlemrinv  26868  nepss  27325  fprod0diag  27448  dfpo2  27516  dfon2  27556  distel  27568  elno2  27746  bdayfo  27767  fnimage  27911  altopthsn  27943  ellines  28134  rankeq1o  28160  df3nandALT1  28194  wl-nfnbi  28306  wl-exeq  28314  wl-aleq  28315  wl-nfeqfb  28317  wl-lem-moreduce  28347  wl-ax11-lem6  28359  volsupnfl  28389  dvtanlem  28394  opnrebl2  28469  locfindis  28530  cover2  28560  isbnd3  28636  cntotbnd  28648  heibor  28673  isfld2  28758  isfldidl  28821  orfa  28835  prtlem16  28967  ismrc  28990  isnacs3  28999  rexzrexnn0  29095  eldioph4b  29103  dford3  29330  wopprc  29332  ttac  29338  pw2f1ocnv  29339  dfac11  29368  dfac21  29372  isnumbasabl  29415  isnumbasgrp  29416  dfacbasgrp  29417  aaitgo  29472  pm10.55  29574  pm11.57  29595  sbeqalbi  29607  pm13.192  29617  pm13.194  29619  ipo0  29658  ifr0  29659  xpexb  29663  reuan  29957  afvfv0bi  30011  ffnafv  30030  eldmeldmressn  30093  f1oexbi  30109  wlkcpr  30243  usg2spthonot1  30362  eclclwwlkn1  30459  clwlknclwlkdifs  30531  frgra0v  30538  isnzr2hash  30725  3impexp  31042  3impexpbicom  31043  com3rgbi  31106  pm2.43bgbi  31109  pm2.43cbi  31110  sb5ALT  31117  trsbc  31134  2pm13.193  31148  ax6e2ndeq  31155  2uasbanh  31157  eelT01  31326  eel0T1  31327  uunT1  31400  zfregs2VD  31464  equncomVD  31491  trsbcVD  31500  undif3VD  31505  2pm13.193VD  31526  ax6e2eqVD  31530  ax6e2ndeqVD  31532  2uasbanhVD  31534  ax6e2ndeqALT  31554  bnj1533  31732  bnj983  31831  bj-dfbi6  31964  bj-dfif5ALT  31971  bj-consensus  31984  bj-andnotim  31993  bj-cbvalv  32089  bj-equsexv  32105  bj-equs45fv  32123  bj-sb6  32142  bj-axext4  32147  bj-cleqh  32150  bj-hbaeb  32183  bj-hbnaeb  32184  bj-equsal  32190  bj-dfcleq  32250  bj-csbsnlem  32254  bj-snsetex  32303  bj-snglex  32313  bj-1uplth  32347  bj-1uplex  32348  bj-2uplth  32361  bj-2uplex  32362  isltrn2N  33604