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  444  ancom  448  oridm  511  orbi2i  516  or12  520  pm4.45im  557  pm4.44  572  pm4.79  578  anass  642  jaob  774  jcab  851  andi  855  pm4.72  864  oibabs  869  pm4.82  912  consensus  943  rnlem  949  cases2  956  3jaob  1273  truanOLD  1380  dfnotOLD  1382  3impexp  1413  3impexpbicom  1414  cad1  1443  tbw-bijust  1508  tbw-negdf  1509  19.26  1647  sbbii  1706  19.9v  1716  equcom  1731  equvin  1741  cbvalw  1745  alcom  1782  19.3  1820  19.41  1897  cbval  1968  equsex  1985  equvinOLD  2039  equs45f  2040  dfsb2  2061  sb6f  2073  sbnOLD  2081  sbim  2085  sb5rfOLD  2123  sb6rfOLD  2125  sb9OLD  2131  sb6  2135  mo2v  2260  exmoeu  2286  exmoeuOLD  2287  mo3  2292  mo3OLD  2293  moOLD  2300  eu2OLD  2302  mo2OLD  2309  moanim  2327  euan  2328  euanOLD  2329  2mo  2355  2moOLD  2356  2eu6  2363  axext4  2417  cleqh  2530  nebi  2672  r19.26  2839  ralcom3  2876  ceqsex  2997  gencbvex  3005  gencbvex2  3006  eqvinc  3075  pm13.183  3089  rr19.3v  3090  rr19.28v  3091  euxfr2  3133  reu6  3137  reu3  3138  sspss  3443  unineq  3588  uneqin  3589  undif3  3599  difrab  3612  sbnfc2  3694  un00  3702  ssdifeq0  3749  r19.2zb  3758  ralf0  3774  elpr2  3884  snidb  3892  rabsnifsb  3931  tppreqb  4002  difsnb  4003  pwpw0  4009  sssn  4019  preq12b  4036  preqsn  4043  pwsnALT  4074  unissint  4140  uniintsn  4153  iununi  4243  intex  4436  intnex  4437  iin0  4454  axpweq  4457  eusvnfb  4476  eusv2nf  4478  ralxfrALT  4499  nfcvb  4510  sspwb  4529  unipw  4530  opnz  4551  opth  4554  opthwiener  4581  ssopab2b  4604  pwssun  4614  elon2  4717  opelxp  4856  opthprc  4873  relop  4977  issetid  4981  xpid11  5048  elres  5133  iss  5142  restidsing  5150  issref  5199  asymref2  5203  xpnz  5245  xpdifid  5254  ssrnres  5264  dfrel2  5276  relrelss  5349  unixp0  5359  fn0  5518  funssxp  5559  f00  5581  f0bi  5582  dffo2  5612  f1o00  5661  fo00  5662  fv3  5691  dffn5  5725  dff2  5843  dff3  5844  dffo4  5847  dffo5  5848  exfo  5849  fmpt  5852  ffnfv  5856  fsn  5868  fsn2  5870  fnsnb  5885  fconstfv  5927  isores1  6012  ssoprab2b  6132  eqfnov2  6186  unexb  6369  uniexb  6375  iunpw  6379  ordeleqon  6389  onintrab  6401  unon  6431  onuninsuci  6440  ordzsl  6445  onzsl  6446  ffoss  6527  1st2ndb  6603  suppssov1  6710  suppssfv  6714  reldmtpos  6742  abianfp  6900  omopthi  7084  mapsn  7242  mapsncnv  7247  mptelixpg  7288  elixpsn  7290  ixpsnf1o  7291  bren2  7328  en0  7360  en1  7364  en1b  7365  sbthb  7420  canth2  7452  onfin2  7490  sdom1  7500  1sdom  7503  fineqv  7516  unfilem1  7564  fiint  7576  pwfi  7594  unifpw  7602  wofib  7747  sucprcreg  7802  sucprcregOLD  7803  opthreg  7812  suc11reg  7813  infeq5  7831  rankwflemb  7988  r1elss  8001  pwwf  8002  unwf  8005  uniwf  8014  rankonid  8024  rankr1id  8057  rankuni  8058  rankxplim3  8076  scott0  8081  karden  8090  isnum3  8112  oncard  8118  card1  8126  cardlim  8130  cardmin2  8156  pm54.43lem  8157  ween  8193  acnnum  8210  alephsuc2  8238  alephgeom  8240  iscard3  8251  dfac3  8279  dfac4  8280  dfac5lem3  8283  dfac5  8286  dfac2  8288  dfac8  8292  dfac9  8293  dfacacn  8298  dfac13  8299  dfac12r  8303  dfac12k  8304  kmlem2  8308  kmlem13  8319  cdainf  8349  ackbij2  8400  cflim2  8420  isfin4-2  8471  isfin4-3  8472  isf33lem  8523  compsscnv  8528  fin1a2lem6  8562  domtriom  8600  ac9  8640  ac9s  8650  fodomb  8681  brdom3  8683  brdom5  8684  brdom4  8685  brdom7disj  8686  brdom6disj  8687  iunfo  8691  sdomsdomcard  8712  gch2  8830  gch3  8831  eltsk2g  8906  grutsk  8977  grothpw  8981  ordpipq  9099  ltbtwnnq  9135  mappsrpr  9263  map2psrpr  9265  elreal2  9287  le2tri3i  9492  ltadd2i  9493  elnn0nn  10610  elnnnn0b  10612  elnnnn0c  10613  elnnz  10644  elnn0z  10647  elz2  10651  elnnz1  10660  eluz2b2  10915  elnn1uz2  10919  elioo4g  11344  eluzfz2b  11447  fzn0  11451  elfz1end  11466  fzass4  11483  nn0fz0  11509  elfz1b  11511  fzolb  11542  fzon0  11553  elfzo0  11571  fzo1fzo0n0  11572  elfzo0z  11573  elfzo1  11579  om2uzrani  11759  nn0opthi  12032  hashkf  12089  hashprb  12141  hashf1  12194  iswrdbi  12225  wrdexb  12229  0wrd0  12237  sqr0lem  12714  rexanuz  12817  rexuz3  12820  fsum0diag  13228  sadcp1  13634  isprm6  13778  4sqlem4  13996  mreunirn  14522  isdrs2  15092  isacs5  15325  isacs4  15326  isacs3  15327  isnsg3  15695  gicer  15784  oppgmndb  15850  oppggrpb  15853  pmtrfb  15951  invghm  16298  opprrngb  16658  abvn0b  17296  funsnfsupOLD  17569  gzrngunit  17722  dvdsrzring  17743  dvdsrz  17744  zringunit  17756  zrngunit  17757  zlmlmod  17796  zlmassa  17797  cygth  17846  frgpcyg  17848  tgclb  18417  iscldtop  18541  isnrm2  18804  isnrm3  18805  discmp  18843  dfcon2  18865  2ndcsb  18895  dis2ndc  18906  loclly  18933  iskgen2  18963  dfac14  19033  kqtop  19160  kqt0  19161  kqreg  19166  kqnrm  19167  hmpher  19199  hmphsymb  19201  hmph0  19210  kqhmph  19234  ist1-5lem  19235  elmptrab2  19243  isfil2  19271  filunirn  19297  isufil2  19323  hausflim  19396  isfcls  19424  alexsubALT  19465  istgp2  19504  ustbas  19644  xmetunirn  19754  dscmet  20007  dscopn  20008  isngp4  20045  zcld  20232  zlmclm  20509  iscmet2  20647  iundisj  20871  i1f1lem  21009  fta1b  21526  elply2  21549  elqaa  21673  aannenlem2  21680  wilth  22294  lgsne0  22557  2sqlem2  22588  ostth  22773  mptelee  22964  uhgra0v  23067  wrdumgra  23073  usgra0v  23113  uvtx01vtx  23223  istrl2  23260  isspthonpth  23306  nmlno0lem  24016  isblo3i  24024  blocni  24028  hvsubeq0i  24288  hvaddcani  24290  bcseqi  24345  isch3  24467  norm1exi  24476  hhsssh  24493  shslubi  24611  dfch2  24633  pjoc1i  24657  pjchi  24658  shs00i  24676  chsscon3i  24687  chlejb1i  24702  chj00i  24713  shjshseli  24719  h1de2ctlem  24781  spanunsni  24805  cmcmi  24818  cmbr3i  24826  cmbr4i  24827  pj11i  24937  hosubeq0i  25053  dmadjrnb  25133  nmlnop0iALT  25222  lnopeq0i  25234  elunop2  25240  lnconi  25260  lncnopbd  25264  adjbdlnb  25311  adjbd1o  25312  adjeq0  25318  rnbra  25334  pjss1coi  25390  pjss2coi  25391  pjnormssi  25395  pjssdif2i  25401  pjssdif1i  25402  dfpjop  25409  pjinvari  25418  pjin2i  25420  pjci  25427  pjcmul1i  25428  pjcmul2i  25429  strb  25485  hstrbi  25493  mdsl1i  25548  atom1d  25580  chrelat2i  25592  cvbr4i  25594  cvexchi  25596  sumdmdi  25647  dmdbr4ati  25648  dmdbr5ati  25649  dmdbr6ati  25650  dmdbr7ati  25651  cdj3i  25668  difeq  25723  iundisjf  25755  cnvoprab  25847  fpwrelmap  25858  iundisjfi  25903  xrge0tsmsbi  26107  issgon  26420  measbasedom  26470  oddpwdc  26585  eulerpartlemt  26602  ballotlem2  26719  ballotlemrinv  26764  nepss  27221  fprod0diag  27344  dfpo2  27412  dfon2  27452  distel  27464  elno2  27642  bdayfo  27663  fnimage  27807  altopthsn  27839  ellines  28030  rankeq1o  28056  df3nandALT1  28090  wl-nfnbi  28203  wl-nfae1  28204  wl-exeq  28211  wl-aleq  28212  wl-nfeqfb  28214  wl-ax11-lem6  28250  volsupnfl  28280  dvtanlem  28285  opnrebl2  28360  locfindis  28421  cover2  28451  isbnd3  28527  cntotbnd  28539  heibor  28564  isfld2  28649  isfldidl  28712  orfa  28726  prtlem16  28859  ismrc  28882  isnacs3  28891  rexzrexnn0  28987  eldioph4b  28995  dford3  29222  wopprc  29224  ttac  29230  pw2f1ocnv  29231  dfac11  29260  dfac21  29264  isnumbasabl  29307  isnumbasgrp  29308  dfacbasgrp  29309  aaitgo  29364  pm10.55  29466  pm11.57  29487  sbeqalbi  29499  pm13.192  29509  pm13.194  29511  ipo0  29550  ifr0  29551  xpexb  29555  reuan  29850  afvfv0bi  29904  ffnafv  29923  eldmeldmressn  29986  f1oexbi  30002  wlkcpr  30136  usg2spthonot1  30255  eclclwwlkn1  30352  clwlknclwlkdifs  30424  frgra0v  30431  isnzr2hash  30605  com3rgbi  30920  pm2.43bgbi  30923  pm2.43cbi  30924  sb5ALT  30931  trsbc  30948  2pm13.193  30962  ax6e2ndeq  30969  2uasbanh  30971  eelT01  31141  eel0T1  31142  uunT1  31215  zfregs2VD  31279  equncomVD  31306  trsbcVD  31315  undif3VD  31320  2pm13.193VD  31341  ax6e2eqVD  31345  ax6e2ndeqVD  31347  2uasbanhVD  31349  ax6e2ndeqALT  31369  bnj1533  31547  bnj983  31646  bj-andnotim  31776  bj-cbvalv  31863  bj-equsexv  31879  bj-cleqh  31915  bj-aecom  31945  bj-hbaeb  31947  bj-hbnaeb  31948  bj-equsal  31954  bj-dfcleq  31995  bj-csbsnlem  31999  bj-snsetex  32039  bj-snglex  32049  bj-1uplth  32083  bj-1uplex  32084  bj-2uplth  32097  bj-2uplex  32098  isltrn2N  33337