Theorem impbii 190

Description: Infer an equivalence from an implication and its converse. Inference associated with impbi 189. (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		impbi 189	. 2 |- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )
4	1, 2, 3	mp2 9	1 |- ( ph <-> ps )

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

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 188

This theorem is referenced by:  dfbi1  194  bicom  203  biid  239  2th  242  pm5.74  247  bitri  252  notnot  292  con34b  293  notbi  296  bibi2i  314  con1b  334  con2b  335  bi2.04  362  pm5.4  363  imdi  364  pm4.8  366  pm4.81  367  orcom  388  dfor2  412  impexp  447  ancom  451  oridm  516  orbi2i  521  or12  525  pm4.45im  564  pm4.44  579  pm4.79  585  anass  653  jaob  790  jcab  871  andi  875  pm4.72  884  oibabs  889  pm4.82  936  consensus  967  rnlemOLD  973  cases2  980  3impexp  1227  3jaob  1326  truanOLD  1455  dfnotOLD  1457  tbw-bijust  1577  tbw-negdf  1578  19.26  1727  19.35  1734  19.21v  1778  19.21vOLDOLD  1779  sbbii  1796  19.9v  1804  19.23v  1810  19.41v  1822  equcom  1846  equvin  1856  cbvalw  1860  alcom  1897  19.3  1941  19.41  2028  cbval  2077  equsex  2093  aecom  2107  equs45f  2145  dfsb2  2168  sb6f  2180  sbim  2190  sb6  2225  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  exmoeu  2300  mo3  2306  moanim  2328  euan  2329  2mo  2351  2moOLD  2352  2eu6  2361  2eu6OLD  2362  axext4  2411  eqcom  2438  cleqhOLD  2545  nebi  2741  r19.26  2962  ralcom3  3001  ceqsex  3123  gencbvex  3131  gencbvex2  3132  eqvinc  3204  pm13.183  3218  rr19.3v  3219  rr19.28v  3220  euxfr2  3262  reu6  3266  reu3  3267  sspss  3570  unineq  3729  uneqin  3730  undif3  3740  difrab  3753  sbnfc2  3830  un00  3834  ssdifeq0  3884  r19.2zb  3893  ralf0  3910  elpr2  4021  snidb  4029  rabsnifsb  4071  tppreqb  4144  difsnb  4145  pwpw0  4151  sssn  4161  preq12b  4179  preqsn  4186  pwsnALT  4217  unissint  4283  uniintsn  4296  iununi  4390  intex  4581  intnex  4582  iin0  4599  axpweq  4602  eusvnfb  4621  eusv2nf  4623  ralxfrALT  4641  nfcvb  4652  sspwb  4671  unipw  4672  opnz  4693  opth  4696  opthwiener  4723  ssopab2b  4748  pwssun  4760  opelxp  4884  opthprc  4902  relop  5005  issetid  5009  xpid11  5076  elres  5160  eldmeldmressn  5165  iss  5172  restidsing  5181  issref  5233  asymref2  5237  xpnz  5276  xpdifid  5285  ssrnres  5295  dfrel2  5306  relrelss  5379  unixp0  5390  elon2  5453  fn0  5713  funssxp  5759  f00  5782  f0bi  5783  dffo2  5814  f1o00  5863  fo00  5864  fv3  5894  dffn5  5926  dff2  6049  dff3  6050  dffo4  6053  dffo5  6054  exfo  6055  fmpt  6058  ffnfv  6064  fsn  6076  fsn2  6077  fnsnb  6098  fconstfvOLD  6142  isores1  6240  ssoprab2b  6362  eqfnov2  6417  unexb  6605  uniexb  6615  iunpw  6619  ordeleqon  6629  onintrab  6642  unon  6672  onuninsuci  6681  ordzsl  6686  onzsl  6687  f1oexbi  6757  ffoss  6768  1st2ndb  6845  suppssov1  6958  suppssfv  6962  reldmtpos  6989  dfrecs3  7099  omopthi  7366  mapsn  7521  mapsncnv  7526  mptelixpg  7567  elixpsn  7569  ixpsnf1o  7570  bren2  7607  en0  7639  en1  7643  en1b  7644  sbthb  7699  canth2  7731  onfin2  7770  sdom1  7778  1sdom  7781  fineqv  7793  unfilem1  7841  fiint  7854  pwfi  7875  unifpw  7883  wofib  8060  sucprcreg  8114  opthreg  8123  suc11reg  8124  infeq5  8142  rankwflemb  8263  r1elss  8276  pwwf  8277  unwf  8280  uniwf  8289  rankonid  8299  rankr1id  8332  rankuni  8333  rankxplim3  8351  scott0  8356  karden  8365  isnum3  8387  oncard  8393  card1  8401  cardlim  8405  cardmin2  8431  pm54.43lem  8432  ween  8464  acnnum  8481  alephsuc2  8509  alephgeom  8511  iscard3  8522  dfac3  8550  dfac4  8551  dfac5lem3  8554  dfac5  8557  dfac2  8559  dfac8  8563  dfac9  8564  dfacacn  8569  dfac13  8570  dfac12r  8574  dfac12k  8575  kmlem2  8579  kmlem13  8590  cdainf  8620  ackbij2  8671  cflim2  8691  isfin4-2  8742  isfin4-3  8743  isf33lem  8794  compsscnv  8799  fin1a2lem6  8833  domtriom  8871  ac9  8911  ac9s  8921  fodomb  8952  brdom3  8954  brdom5  8955  brdom4  8956  brdom7disj  8957  brdom6disj  8958  iunfo  8962  sdomsdomcard  8983  gch2  9099  gch3  9100  eltsk2g  9175  grutsk  9246  grothpw  9250  ordpipq  9366  ltbtwnnq  9402  mappsrpr  9531  map2psrpr  9533  elreal2  9555  le2tri3i  9763  ltadd2iOLD  9765  elnn0nn  10912  elnnnn0b  10914  elnnnn0c  10915  elnnz  10947  elnn0z  10950  elz2  10954  elnnz1  10963  eluz2b2  11231  elnn1uz2  11235  elioo4g  11695  eluzfz2b  11806  fzn0  11811  elfz1end  11827  fzass4  11834  elfz1b  11862  nn0fz0  11888  fzolb  11924  fzon0  11935  elfzo0  11954  fzo1fzo0n0  11955  elfzo0z  11956  elfzo1  11962  om2uzrani  12163  nn0opthi  12453  hashkf  12514  isfinite4  12540  hashprb  12571  hashf1  12615  iswrdb  12664  wrdexb  12670  0wrd0  12680  cotr2g  13019  trclun  13057  sqr0lem  13283  rexanuz  13387  rexuz3  13390  fsum0diag  13816  fprod0diag  14018  sadcp1  14403  isprm6  14637  4sqlem4  14859  mreunirn  15458  isdrs2  16135  isacs5  16369  isacs4  16370  isacs3  16371  isnsg3  16802  gicer  16891  oppgmndb  16957  oppggrpb  16960  pmtrfb  17057  invghm  17409  opprringb  17795  isnzr2hash  18423  abvn0b  18461  gzrngunit  18968  dvdsrzring  18986  zringunit  18993  zlmlmod  19025  zlmassa  19026  cygth  19073  frgpcyg  19075  tgclb  19917  iscldtop  20042  isnrm2  20305  isnrm3  20306  discmp  20344  dfcon2  20365  2ndcsb  20395  dis2ndc  20406  loclly  20433  unisngl  20473  locfindis  20476  iskgen2  20494  dfac14  20564  kqtop  20691  kqt0  20692  kqreg  20697  kqnrm  20698  hmpher  20730  hmphsymb  20732  hmph0  20741  kqhmph  20765  ist1-5lem  20766  elmptrab2  20774  isfil2  20802  filunirn  20828  isufil2  20854  hausflim  20927  isfcls  20955  alexsubALT  20997  istgp2  21037  ustbas  21173  xmetunirn  21283  dscmet  21518  dscopn  21519  isngp4  21556  zcld  21742  zlmclm  22019  iscmet2  22157  iundisj  22378  i1f1lem  22524  fta1b  22995  elply2  23018  elqaa  23143  aannenlem2  23150  wilth  23861  lgsne0  24124  2sqlem2  24155  ostth  24340  mptelee  24771  uhgra0v  24883  wrdumgra  24889  usgra0v  24944  uvtx01vtx  25065  wlkcpr  25102  isspthonpth  25159  eclclwwlkn1  25405  usg2spthonot1  25463  clwlknclwlkdifs  25533  frgra0v  25566  nmlno0lem  26279  isblo3i  26287  blocni  26291  hvsubeq0i  26551  hvaddcani  26553  bcseqi  26608  isch3  26729  norm1exi  26738  hhsssh  26755  shslubi  26873  dfch2  26895  pjoc1i  26919  pjchi  26920  shs00i  26938  chsscon3i  26949  chlejb1i  26964  chj00i  26975  shjshseli  26981  h1de2ctlem  27043  spanunsni  27067  cmcmi  27080  cmbr3i  27088  cmbr4i  27089  pj11i  27199  hosubeq0i  27314  dmadjrnb  27394  nmlnop0iALT  27483  lnopeq0i  27495  elunop2  27501  lnconi  27521  lncnopbd  27525  adjbdlnb  27572  adjbd1o  27573  adjeq0  27579  rnbra  27595  pjss1coi  27651  pjss2coi  27652  pjnormssi  27656  pjssdif2i  27662  pjssdif1i  27663  dfpjop  27670  pjinvari  27679  pjin2i  27681  pjci  27688  pjcmul1i  27689  pjcmul2i  27690  strb  27746  hstrbi  27754  mdsl1i  27809  atom1d  27841  chrelat2i  27853  cvbr4i  27855  cvexchi  27857  sumdmdi  27908  dmdbr4ati  27909  dmdbr5ati  27910  dmdbr6ati  27911  dmdbr7ati  27912  cdj3i  27929  difeq  27987  iundisjf  28038  cnvoprab  28151  fpwrelmap  28161  iundisjfi  28208  xrge0tsmsbi  28388  issgon  28784  measbasedom  28863  oddpwdc  29013  eulerpartlemt  29030  ballotlem2  29147  ballotlemrinv  29192  bnj1533  29451  bnj983  29550  elmsta  29974  nepss  30138  dfpo2  30182  dfon2  30225  distel  30237  elno2  30328  bdayfo  30349  fnimage  30481  altopthsn  30513  ellines  30704  rankeq1o  30723  opnrebl2  30762  df3nandALT1  30842  pm4.81ALT  30917  bj-dfbi6  30936  bj-consensus  30941  bj-falor2  30953  bj-bibibi  30954  bj-andnotim  30956  bj-cbvexw  31015  bj-cbvalv  31076  bj-equs45fv  31111  bj-sb6  31130  bj-axext4  31135  bj-cleqh  31138  bj-hbaeb2  31171  bj-hbnaeb  31173  bj-equsal  31179  bj-mo3OLD  31198  bj-cleqhyp  31249  bj-csbsnlem  31255  bj-snsetex  31306  bj-snglex  31316  bj-1uplth  31350  bj-1uplex  31351  bj-2uplth  31364  bj-2uplex  31365  bj-elid  31384  bj-elid3  31386  bj-eldiag2  31392  mptsnunlem  31474  topdifinf  31486  wl-nfnbi  31566  wl-exeq  31574  wl-aleq  31575  wl-nfeqfb  31577  wl-ax11-lem6  31623  volsupnfl  31688  dvtanlemOLD  31694  cover2  31743  isbnd3  31819  cntotbnd  31831  heibor  31856  isfld2  31941  isfldidl  32004  orfa  32018  prtlem16  32148  isltrn2N  33393  ismrc  35251  isnacs3  35260  rexzrexnn0  35355  eldioph4b  35362  dford3  35588  wopprc  35590  ttac  35596  pw2f1ocnv  35597  dfac11  35625  dfac21  35629  isnumbasabl  35670  isnumbasgrp  35671  dfacbasgrp  35672  aaitgo  35726  ifpbi1b  35845  rp-fakeimass  35854  rp-fakeanorass  35855  rp-fakenanass  35857  rp-isfinite5  35860  rp-isfinite6  35861  cnvtrrel  35900  rp-imass  36002  frege54cor0a  36095  nanorxor  36289  nzss  36302  pm10.55  36354  pm11.57  36375  sbeqalbi  36387  pm13.192  36397  pm13.194  36399  ipo0  36438  ifr0  36439  xpexb  36443  3impexpbicom  36470  com3rgbi  36507  pm2.43bgbi  36510  pm2.43cbi  36511  sb5ALT  36518  trsbc  36537  2pm13.193  36555  ax6e2ndeq  36562  2uasbanh  36564  eelT01  36733  eel0T1  36734  uunT1  36806  zfregs2VD  36876  equncomVD  36904  trsbcVD  36913  undif3VD  36918  2pm13.193VD  36939  ax6e2eqVD  36943  ax6e2ndeqVD  36945  2uasbanhVD  36947  ax6e2ndeqALT  36967  fompt  37089  elfzfzo  37094  dvnprodlem3  37391  elaa2  37665  sge00  37751  ismea  37797  confun  37919  reuan  37991  afvfv0bi  38043  ffnafv  38062  residfi  38387  mgm2mgm  38620  isringrng  38638  nnpw2pb  39158