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  289  con34b  290  notbi  293  bibi2i  311  con1b  331  con2b  332  bi2.04  359  pm5.4  360  imdi  361  pm4.8  363  pm4.81  364  orcom  385  dfor2  409  impexp  444  ancom  448  oridm  512  orbi2i  517  or12  521  pm4.45im  560  pm4.44  575  pm4.79  581  anass  647  jaob  781  jcab  861  andi  865  pm4.72  874  oibabs  879  pm4.82  926  consensus  957  rnlemOLD  963  cases2  969  3jaob  1288  truanOLD  1417  dfnotOLD  1419  cad1OLD  1473  tbw-bijust  1538  tbw-negdf  1539  19.26  1688  19.35  1695  19.21v  1737  sbbii  1754  19.9v  1762  19.23v  1768  19.41v  1779  equcom  1802  equvin  1812  cbvalw  1816  alcom  1853  19.3  1896  19.41  1979  cbval  2028  equsex  2044  aecom  2057  equs45f  2095  dfsb2  2118  sb6f  2130  sbim  2140  sb6  2177  mo2v  2225  mo2vOLD  2226  mo2vOLDOLD  2227  exmoeu  2252  mo3  2258  mo3OLD  2259  moanim  2281  euan  2282  2mo  2304  2moOLD  2305  2eu6  2314  2eu6OLD  2315  axext4  2364  eqcom  2391  cleqhOLD  2498  nebi  2692  r19.26  2909  ralcom3  2948  ceqsex  3070  gencbvex  3078  gencbvex2  3079  eqvinc  3151  pm13.183  3165  rr19.3v  3166  rr19.28v  3167  euxfr2  3209  reu6  3213  reu3  3214  sspss  3517  unineq  3673  uneqin  3674  undif3  3684  difrab  3697  sbnfc2  3774  un00  3778  ssdifeq0  3826  r19.2zb  3835  ralf0  3852  elpr2  3963  snidb  3971  rabsnifsb  4012  tppreqb  4085  difsnb  4086  pwpw0  4092  sssn  4102  preq12b  4120  preqsn  4127  pwsnALT  4158  unissint  4224  uniintsn  4237  iununi  4331  intex  4521  intnex  4522  iin0  4539  axpweq  4542  eusvnfb  4561  eusv2nf  4563  ralxfrALT  4581  nfcvb  4592  sspwb  4611  unipw  4612  opnz  4633  opth  4636  opthwiener  4663  ssopab2b  4688  pwssun  4700  elon2  4803  opelxp  4943  opthprc  4961  relop  5066  issetid  5070  xpid11  5137  elres  5221  eldmeldmressn  5226  iss  5233  restidsing  5242  issref  5293  asymref2  5297  xpnz  5336  xpdifid  5345  ssrnres  5355  dfrel2  5366  relrelss  5439  unixp0  5450  fn0  5608  funssxp  5652  f00  5675  f0bi  5676  dffo2  5707  f1o00  5756  fo00  5757  fv3  5787  dffn5  5819  dff2  5945  dff3  5946  dffo4  5949  dffo5  5950  exfo  5951  fmpt  5954  ffnfv  5959  fsn  5971  fsn2  5973  fnsnb  5992  fconstfvOLD  6035  isores1  6131  ssoprab2b  6253  eqfnov2  6308  unexb  6499  uniexb  6509  iunpw  6513  ordeleqon  6523  onintrab  6535  unon  6565  onuninsuci  6574  ordzsl  6579  onzsl  6580  f1oexbi  6649  ffoss  6660  1st2ndb  6737  suppssov1  6850  suppssfv  6854  reldmtpos  6881  omopthi  7224  mapsn  7379  mapsncnv  7384  mptelixpg  7425  elixpsn  7427  ixpsnf1o  7428  bren2  7465  en0  7497  en1  7501  en1b  7502  sbthb  7557  canth2  7589  onfin2  7628  sdom1  7636  1sdom  7639  fineqv  7651  unfilem1  7699  fiint  7712  pwfi  7730  unifpw  7738  wofib  7885  sucprcreg  7940  opthreg  7949  suc11reg  7950  infeq5  7968  rankwflemb  8124  r1elss  8137  pwwf  8138  unwf  8141  uniwf  8150  rankonid  8160  rankr1id  8193  rankuni  8194  rankxplim3  8212  scott0  8217  karden  8226  isnum3  8248  oncard  8254  card1  8262  cardlim  8266  cardmin2  8292  pm54.43lem  8293  ween  8329  acnnum  8346  alephsuc2  8374  alephgeom  8376  iscard3  8387  dfac3  8415  dfac4  8416  dfac5lem3  8419  dfac5  8422  dfac2  8424  dfac8  8428  dfac9  8429  dfacacn  8434  dfac13  8435  dfac12r  8439  dfac12k  8440  kmlem2  8444  kmlem13  8455  cdainf  8485  ackbij2  8536  cflim2  8556  isfin4-2  8607  isfin4-3  8608  isf33lem  8659  compsscnv  8664  fin1a2lem6  8698  domtriom  8736  ac9  8776  ac9s  8786  fodomb  8817  brdom3  8819  brdom5  8820  brdom4  8821  brdom7disj  8822  brdom6disj  8823  iunfo  8827  sdomsdomcard  8848  gch2  8964  gch3  8965  eltsk2g  9040  grutsk  9111  grothpw  9115  ordpipq  9231  ltbtwnnq  9267  mappsrpr  9396  map2psrpr  9398  elreal2  9420  le2tri3i  9625  ltadd2iOLD  9627  elnn0nn  10755  elnnnn0b  10757  elnnnn0c  10758  elnnz  10791  elnn0z  10794  elz2  10798  elnnz1  10807  eluz2b2  11073  elnn1uz2  11077  elioo4g  11506  eluzfz2b  11616  fzn0  11621  elfz1end  11636  fzass4  11643  elfz1b  11670  nn0fz0  11696  fzolb  11728  fzon0  11739  elfzo0  11758  fzo1fzo0n0  11759  elfzo0z  11760  elfzo1  11766  om2uzrani  11966  nn0opthi  12252  hashkf  12309  isfinite4  12335  hashprb  12366  hashf1  12410  iswrdb  12459  wrdexb  12465  0wrd0  12475  cotr2g  12814  trclun  12852  sqr0lem  13076  rexanuz  13180  rexuz3  13183  fsum0diag  13594  fprod0diag  13792  sadcp1  14107  isprm6  14252  4sqlem4  14472  mreunirn  15008  isdrs2  15685  isacs5  15919  isacs4  15920  isacs3  15921  isnsg3  16352  gicer  16441  oppgmndb  16507  oppggrpb  16510  pmtrfb  16607  invghm  16959  opprringb  17394  isnzr2hash  18025  abvn0b  18064  funsnfsupOLD  18369  gzrngunit  18596  dvdsrzring  18614  zringunit  18621  zlmlmod  18653  zlmassa  18654  cygth  18701  frgpcyg  18703  tgclb  19557  iscldtop  19682  isnrm2  19945  isnrm3  19946  discmp  19984  dfcon2  20005  2ndcsb  20035  dis2ndc  20046  loclly  20073  unisngl  20113  locfindis  20116  iskgen2  20134  dfac14  20204  kqtop  20331  kqt0  20332  kqreg  20337  kqnrm  20338  hmpher  20370  hmphsymb  20372  hmph0  20381  kqhmph  20405  ist1-5lem  20406  elmptrab2  20414  isfil2  20442  filunirn  20468  isufil2  20494  hausflim  20567  isfcls  20595  alexsubALT  20636  istgp2  20675  ustbas  20815  xmetunirn  20925  dscmet  21178  dscopn  21179  isngp4  21216  zcld  21403  zlmclm  21680  iscmet2  21818  iundisj  22043  i1f1lem  22181  fta1b  22655  elply2  22678  elqaa  22803  aannenlem2  22810  wilth  23462  lgsne0  23725  2sqlem2  23756  ostth  23941  mptelee  24319  uhgra0v  24431  wrdumgra  24437  usgra0v  24492  uvtx01vtx  24613  wlkcpr  24650  isspthonpth  24707  eclclwwlkn1  24953  usg2spthonot1  25011  clwlknclwlkdifs  25081  frgra0v  25114  nmlno0lem  25825  isblo3i  25833  blocni  25837  hvsubeq0i  26097  hvaddcani  26099  bcseqi  26154  isch3  26276  norm1exi  26285  hhsssh  26302  shslubi  26420  dfch2  26442  pjoc1i  26466  pjchi  26467  shs00i  26485  chsscon3i  26496  chlejb1i  26511  chj00i  26522  shjshseli  26528  h1de2ctlem  26590  spanunsni  26614  cmcmi  26627  cmbr3i  26635  cmbr4i  26636  pj11i  26746  hosubeq0i  26861  dmadjrnb  26941  nmlnop0iALT  27030  lnopeq0i  27042  elunop2  27048  lnconi  27068  lncnopbd  27072  adjbdlnb  27119  adjbd1o  27120  adjeq0  27126  rnbra  27142  pjss1coi  27198  pjss2coi  27199  pjnormssi  27203  pjssdif2i  27209  pjssdif1i  27210  dfpjop  27217  pjinvari  27226  pjin2i  27228  pjci  27235  pjcmul1i  27236  pjcmul2i  27237  strb  27293  hstrbi  27301  mdsl1i  27356  atom1d  27388  chrelat2i  27400  cvbr4i  27402  cvexchi  27404  sumdmdi  27455  dmdbr4ati  27456  dmdbr5ati  27457  dmdbr6ati  27458  dmdbr7ati  27459  cdj3i  27476  difeq  27534  iundisjf  27578  cnvoprab  27696  fpwrelmap  27706  iundisjfi  27754  xrge0tsmsbi  27930  issgon  28272  measbasedom  28329  oddpwdc  28476  eulerpartlemt  28493  ballotlem2  28610  ballotlemrinv  28655  elmsta  29097  nepss  29261  dfpo2  29350  dfon2  29389  distel  29401  elno2  29579  bdayfo  29600  fnimage  29732  altopthsn  29764  ellines  29955  rankeq1o  29981  df3nandALT1  30015  wl-nfnbi  30144  wl-exeq  30152  wl-aleq  30153  wl-nfeqfb  30155  wl-ax11-lem6  30195  volsupnfl  30224  dvtanlemOLD  30230  opnrebl2  30305  cover2  30370  isbnd3  30446  cntotbnd  30458  heibor  30483  isfld2  30568  isfldidl  30631  orfa  30645  prtlem16  30776  ismrc  30799  isnacs3  30808  rexzrexnn0  30903  eldioph4b  30910  dford3  31136  wopprc  31138  ttac  31144  pw2f1ocnv  31145  dfac11  31174  dfac21  31178  isnumbasabl  31223  isnumbasgrp  31224  dfacbasgrp  31225  aaitgo  31279  nanorxor  31353  nzss  31390  pm10.55  31442  pm11.57  31463  sbeqalbi  31475  pm13.192  31485  pm13.194  31487  ipo0  31526  ifr0  31527  xpexb  31531  elfzfzo  31625  dvnprodlem3  31911  elaa2  32183  reuan  32351  afvfv0bi  32403  ffnafv  32422  residfi  32635  mgm2mgm  32869  isringrng  32887  nnpw2pb  33408  3impexp  33553  3impexpbicom  33554  com3rgbi  33617  pm2.43bgbi  33620  pm2.43cbi  33621  sb5ALT  33628  trsbc  33647  2pm13.193  33665  ax6e2ndeq  33672  2uasbanh  33674  eelT01  33843  eel0T1  33844  uunT1  33917  zfregs2VD  33987  equncomVD  34015  trsbcVD  34024  undif3VD  34029  2pm13.193VD  34050  ax6e2eqVD  34054  ax6e2ndeqVD  34056  2uasbanhVD  34058  ax6e2ndeqALT  34078  bnj1533  34257  bnj983  34356  pm4.81ALT  34483  bj-dfbi6  34503  bj-consensus  34510  bj-falor2  34521  bj-bibibi  34522  bj-andnotim  34524  bj-cbvexw  34582  bj-cbvalv  34643  bj-equsexv  34659  bj-equsexvv  34660  bj-equs45fv  34678  bj-sb6  34697  bj-axext4  34702  bj-cleqh  34705  bj-hbaeb2  34738  bj-hbnaeb  34740  bj-equsal  34746  bj-dfcleq  34813  bj-csbsnlem  34817  bj-snsetex  34869  bj-snglex  34879  bj-1uplth  34913  bj-1uplex  34914  bj-2uplth  34927  bj-2uplex  34928  bj-elid  34947  bj-elid3  34949  bj-eldiag2  34955  isltrn2N  36257  ifpbi1b  38120  rp-fakeimass  38166  rp-fakeanorass  38167  rp-fakenanass  38169  rp-isfinite5  38172  rp-isfinite6  38173  cnvtrrel  38207  rp-imass  38265  frege54cor0a  38362