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  tbw-bijust  1575  tbw-negdf  1576  19.26  1726  19.35  1734  19.21v  1779  19.21vOLDOLD  1780  sbbii  1797  19.9v  1805  19.23v  1811  19.41v  1823  equcom  1848  equvin  1858  cbvalw  1862  alcom  1899  19.3  1943  19.41  2030  cbval  2079  equsex  2095  aecom  2110  equs45f  2148  dfsb2  2171  sb6f  2183  sbim  2193  sb6  2228  mo2v  2276  exmoeu  2301  mo3  2306  moanim  2328  euan  2329  2mo  2350  2eu6  2357  axext4  2405  eqcom  2431  cleqhOLD  2533  nebi  2730  r19.26  2952  ralcom3  2991  ceqsex  3117  gencbvex  3125  gencbvex2  3126  eqvinc  3198  pm13.183  3211  rr19.3v  3212  rr19.28v  3213  euxfr2  3255  reu6  3259  reu3  3260  sspss  3564  unineq  3723  uneqin  3724  undif3  3734  difrab  3747  sbnfc2  3826  un00  3830  ssdifeq0  3880  r19.2zb  3889  ralf0  3906  elpr2  4017  snidb  4025  rabsnifsb  4068  tppreqb  4141  difsnb  4142  pwpw0  4148  sssn  4158  preq12b  4176  preqsn  4183  pwsnALT  4214  unissint  4280  uniintsn  4293  iununi  4387  intex  4580  intnex  4581  iin0  4598  axpweq  4601  eusvnfb  4620  eusv2nf  4622  ralxfrALT  4640  nfcvb  4651  sspwb  4670  unipw  4671  opnz  4692  opth  4695  opthwiener  4722  ssopab2b  4747  pwssun  4759  opelxp  4883  opthprc  4901  relop  5004  issetid  5008  xpid11  5075  elres  5159  eldmeldmressn  5164  iss  5171  restidsing  5180  issref  5232  asymref2  5236  xpnz  5275  xpdifid  5284  ssrnres  5294  dfrel2  5305  relrelss  5378  unixp0  5389  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  6992  dfrecs3  7102  omopthi  7369  mapsn  7524  mapsncnv  7529  mptelixpg  7570  elixpsn  7572  ixpsnf1o  7573  bren2  7610  en0  7642  en1  7646  en1b  7647  sbthb  7702  canth2  7734  onfin2  7773  sdom1  7781  1sdom  7784  fineqv  7796  unfilem1  7844  fiint  7857  pwfi  7878  unifpw  7886  wofib  8069  sucprcreg  8123  opthreg  8132  suc11reg  8133  infeq5  8151  rankwflemb  8272  r1elss  8285  pwwf  8286  unwf  8289  uniwf  8298  rankonid  8308  rankr1id  8341  rankuni  8342  rankxplim3  8360  scott0  8365  karden  8374  isnum3  8396  oncard  8402  card1  8410  cardlim  8414  cardmin2  8440  pm54.43lem  8441  ween  8473  acnnum  8490  alephsuc2  8518  alephgeom  8520  iscard3  8531  dfac3  8559  dfac4  8560  dfac5lem3  8563  dfac5  8566  dfac2  8568  dfac8  8572  dfac9  8573  dfacacn  8578  dfac13  8579  dfac12r  8583  dfac12k  8584  kmlem2  8588  kmlem13  8599  cdainf  8629  ackbij2  8680  cflim2  8700  isfin4-2  8751  isfin4-3  8752  isf33lem  8803  compsscnv  8808  fin1a2lem6  8842  domtriom  8880  ac9  8920  ac9s  8930  fodomb  8961  brdom3  8963  brdom5  8964  brdom4  8965  brdom7disj  8966  brdom6disj  8967  iunfo  8971  sdomsdomcard  8992  gch2  9107  gch3  9108  eltsk2g  9183  grutsk  9254  grothpw  9258  ordpipq  9374  ltbtwnnq  9410  mappsrpr  9539  map2psrpr  9541  elreal2  9563  le2tri3i  9771  ltadd2iOLD  9773  elnn0nn  10919  elnnnn0b  10921  elnnnn0c  10922  elnnz  10954  elnn0z  10957  elz2  10961  elnnz1  10970  eluz2b2  11238  elnn1uz2  11242  elioo4g  11702  eluzfz2b  11815  fzn0  11820  elfz1end  11836  fzass4  11843  elfz1b  11871  nn0fz0  11897  fzolb  11933  fzon0  11944  elfzo0  11963  fzo1fzo0n0  11964  elfzo0z  11965  elfzo1  11971  om2uzrani  12172  nn0opthi  12462  hashkf  12523  isfinite4  12549  hashprb  12580  hashf1  12624  elss2prb  12647  iswrdb  12681  wrdexb  12687  0wrd0  12697  cotr2g  13040  trclun  13078  sqr0lem  13304  rexanuz  13408  rexuz3  13411  fsum0diag  13837  fprod0diag  14039  sadcp1  14428  isprm6  14665  4sqlem4  14895  mreunirn  15506  isdrs2  16183  isacs5  16417  isacs4  16418  isacs3  16419  isnsg3  16850  gicer  16939  oppgmndb  17005  oppggrpb  17008  pmtrfb  17105  invghm  17473  opprringb  17859  isnzr2hash  18487  abvn0b  18525  gzrngunit  19032  dvdsrzring  19050  zringunit  19060  zlmlmod  19092  zlmassa  19093  cygth  19140  frgpcyg  19142  tgclb  19984  iscldtop  20109  isnrm2  20372  isnrm3  20373  discmp  20411  dfcon2  20432  2ndcsb  20462  dis2ndc  20473  loclly  20500  unisngl  20540  locfindis  20543  iskgen2  20561  dfac14  20631  kqtop  20758  kqt0  20759  kqreg  20764  kqnrm  20765  hmpher  20797  hmphsymb  20799  hmph0  20808  kqhmph  20832  ist1-5lem  20833  elmptrab2  20841  isfil2  20869  filunirn  20895  isufil2  20921  hausflim  20994  isfcls  21022  alexsubALT  21064  istgp2  21104  ustbas  21240  xmetunirn  21350  dscmet  21585  dscopn  21586  isngp4  21623  zcld  21829  zlmclm  22124  iscmet2  22262  iundisj  22499  i1f1lem  22645  fta1b  23118  elply2  23148  elqaa  23276  aannenlem2  23283  wilth  23994  lgsne0  24259  2sqlem2  24290  ostth  24475  mptelee  24923  uhgra0v  25035  wrdumgra  25041  usgra0v  25096  uvtx01vtx  25218  wlkcpr  25255  isspthonpth  25312  eclclwwlkn1  25558  usg2spthonot1  25616  clwlknclwlkdifs  25686  frgra0v  25719  nmlno0lem  26432  isblo3i  26440  blocni  26444  hvsubeq0i  26714  hvaddcani  26716  bcseqi  26771  isch3  26892  norm1exi  26901  hhsssh  26918  shslubi  27036  dfch2  27058  pjoc1i  27082  pjchi  27083  shs00i  27101  chsscon3i  27112  chlejb1i  27127  chj00i  27138  shjshseli  27144  h1de2ctlem  27206  spanunsni  27230  cmcmi  27243  cmbr3i  27251  cmbr4i  27252  pj11i  27362  hosubeq0i  27477  dmadjrnb  27557  nmlnop0iALT  27646  lnopeq0i  27658  elunop2  27664  lnconi  27684  lncnopbd  27688  adjbdlnb  27735  adjbd1o  27736  adjeq0  27742  rnbra  27758  pjss1coi  27814  pjss2coi  27815  pjnormssi  27819  pjssdif2i  27825  pjssdif1i  27826  dfpjop  27833  pjinvari  27842  pjin2i  27844  pjci  27851  pjcmul1i  27852  pjcmul2i  27853  strb  27909  hstrbi  27917  mdsl1i  27972  atom1d  28004  chrelat2i  28016  cvbr4i  28018  cvexchi  28020  sumdmdi  28071  dmdbr4ati  28072  dmdbr5ati  28073  dmdbr6ati  28074  dmdbr7ati  28075  cdj3i  28092  difeq  28150  iundisjf  28201  cnvoprab  28314  fpwrelmap  28324  iundisjfi  28378  xrge0tsmsbi  28557  issgon  28953  measbasedom  29032  oddpwdc  29195  eulerpartlemt  29212  ballotlem2  29329  ballotlemrinv  29374  ballotlemrinvOLD  29412  bnj1533  29671  bnj983  29770  elmsta  30194  nepss  30358  dfpo2  30402  dfon2  30445  distel  30457  elno2  30548  bdayfo  30569  fnimage  30701  altopthsn  30733  ellines  30924  rankeq1o  30943  opnrebl2  30982  df3nandALT1  31062  pm4.81ALT  31137  bj-dfbi6  31156  bj-consensus  31161  bj-falor2  31173  bj-bibibi  31174  bj-andnotim  31176  bj-cbvexw  31235  bj-cbvalv  31296  bj-equs45fv  31330  bj-sb6  31349  bj-axext4  31354  bj-cleqh  31357  bj-hbaeb2  31390  bj-hbnaeb  31392  bj-equsal  31398  bj-mo3OLD  31417  bj-cleqhyp  31468  bj-csbsnlem  31474  bj-snsetex  31525  bj-snglex  31535  bj-1uplth  31569  bj-1uplex  31570  bj-2uplth  31583  bj-2uplex  31584  bj-elid  31603  bj-elid3  31605  bj-eldiag2  31611  mptsnunlem  31704  topdifinf  31716  elxp8  31738  finxp1o  31748  wl-nfnbi  31823  wl-exeq  31831  wl-aleq  31832  wl-nfeqfb  31834  wl-ax11-lem6  31884  volsupnfl  31949  dvtanlemOLD  31955  cover2  32004  isbnd3  32080  cntotbnd  32092  heibor  32117  isfld2  32202  isfldidl  32265  orfa  32279  prtlem16  32409  isltrn2N  33654  ismrc  35512  isnacs3  35521  rexzrexnn0  35616  eldioph4b  35623  dford3  35853  wopprc  35855  ttac  35861  pw2f1ocnv  35862  dfac11  35890  dfac21  35894  isnumbasabl  35935  isnumbasgrp  35936  dfacbasgrp  35937  aaitgo  35998  ifpbi1b  36117  rp-fakeimass  36126  rp-fakeanorass  36127  rp-fakenanass  36129  rp-isfinite5  36132  rp-isfinite6  36133  rtrclex  36194  cnvtrrel  36232  rp-imass  36336  frege54cor0a  36429  nanorxor  36623  nzss  36636  pm10.55  36688  pm11.57  36709  sbeqalbi  36721  pm13.192  36731  pm13.194  36733  ipo0  36772  ifr0  36773  xpexb  36777  3impexpbicom  36804  com3rgbi  36841  pm2.43bgbi  36844  pm2.43cbi  36845  sb5ALT  36852  trsbc  36871  2pm13.193  36889  ax6e2ndeq  36896  2uasbanh  36898  eelT01  37067  eel0T1  37068  uunT1  37140  zfregs2VD  37210  equncomVD  37238  trsbcVD  37247  undif3VD  37252  2pm13.193VD  37273  ax6e2eqVD  37277  ax6e2ndeqVD  37279  2uasbanhVD  37281  ax6e2ndeqALT  37301  fompt  37428  elfzfzo  37440  dvnprodlem3  37763  elaa2  38039  sge00  38126  ismea  38197  elhoi  38268  ovn0  38292  confun  38398  reuan  38472  afvfv0bi  38524  ffnafv  38543  clel5  38851  propeqop  38865  funop  38882  funsneqopb  38888  residfi  38893  wrdumgr  39004  usgruspgrb  39059  uvtxa01vtx0  39227  mgm2mgm  39482  isringrng  39500  nnpw2pb  40019