Theorem impbii 192

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

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

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 190

This theorem is referenced by:  dfbi1  196  bicom  205  biid  244  2th  247  pm5.74  252  bitri  257  notnot  297  con34b  298  notbi  301  bibi2i  319  con1b  339  con2b  340  bi2.04  367  pm5.4  368  imdi  369  pm4.8  371  pm4.81  372  orcom  393  dfor2  417  impexp  452  ancom  456  oridm  521  orbi2i  526  or12  530  pm4.45im  569  pm4.44  585  pm4.79  591  anass  659  jaob  797  jcab  879  andi  883  pm4.72  892  oibabs  897  pm4.82  944  consensus  976  rnlemOLD  982  cases2  989  3impexp  1239  3jaob  1339  tbw-bijust  1592  tbw-negdf  1593  19.26  1743  19.35  1751  19.21v  1797  19.21vOLDOLD  1798  sbbii  1815  19.9v  1823  19.23v  1829  19.41v  1841  equcom  1873  equvin  1884  cbvalw  1888  alcom  1934  19.3  1977  19.41  2062  cbvalv1  2075  cbval  2125  equsex  2141  aecom  2156  equs45f  2192  dfsb2  2213  sb6f  2225  sbim  2235  sb6  2269  mo2v  2317  exmoeu  2342  mo3  2347  moanim  2369  euan  2370  2mo  2391  2eu6  2398  axext4  2446  eqcom  2469  nebi  2716  r19.26  2929  ralcom3  2968  ceqsex  3095  gencbvex  3104  gencbvex2  3105  eqvinc  3178  pm13.183  3191  rr19.3v  3192  rr19.28v  3193  euxfr2  3235  reu6  3239  reu3  3240  sspss  3544  unineq  3705  uneqin  3706  undif3  3716  difrab  3729  sbnfc2  3808  un00  3812  ssdifeq0  3862  r19.2zb  3871  ralf0  3888  elpr2  3999  snidb  4007  rabsnifsb  4053  tppreqb  4126  difsnb  4127  pwpw0  4133  sssn  4143  preq12b  4164  preqsn  4173  pwsnALT  4207  unissint  4273  uniintsn  4286  iununi  4380  intex  4573  intnex  4574  iin0  4591  axpweq  4594  eusvnfb  4613  eusv2nf  4615  ralxfrALT  4633  nfcvb  4644  sspwb  4663  unipw  4664  opnz  4687  opth  4690  opthwiener  4717  ssopab2b  4742  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  5717  funssxp  5765  f00  5788  f0bi  5789  dffo2  5820  f1o00  5870  fo00  5871  fv3  5901  dffn5  5933  dff2  6057  dff3  6058  dffo4  6061  dffo5  6062  exfo  6063  fmpt  6066  ffnfv  6072  fsn  6085  fsn2  6086  fnsnb  6107  fconstfvOLD  6152  isores1  6250  ssoprab2b  6375  eqfnov2  6430  unexb  6618  uniexb  6628  iunpw  6632  ordeleqon  6642  onintrab  6655  unon  6685  onuninsuci  6694  ordzsl  6699  onzsl  6700  f1oexbi  6770  ffoss  6781  1st2ndb  6858  suppssov1  6974  suppssfv  6978  reldmtpos  7007  dfrecs3  7117  omopthi  7384  mapsn  7539  mapsncnv  7544  mptelixpg  7585  elixpsn  7587  ixpsnf1o  7588  bren2  7626  en0  7658  en1  7662  en1b  7663  sbthb  7719  canth2  7751  onfin2  7790  sdom1  7798  1sdom  7801  fineqv  7813  unfilem1  7861  fiint  7874  pwfi  7895  unifpw  7903  wofib  8086  sucprcreg  8140  opthreg  8149  suc11reg  8150  infeq5  8168  rankwflemb  8290  r1elss  8303  pwwf  8304  unwf  8307  uniwf  8316  rankonid  8326  rankr1id  8359  rankuni  8360  rankxplim3  8378  scott0  8383  karden  8392  isnum3  8414  oncard  8420  card1  8428  cardlim  8432  cardmin2  8458  pm54.43lem  8459  ween  8492  acnnum  8509  alephsuc2  8537  alephgeom  8539  iscard3  8550  dfac3  8578  dfac4  8579  dfac5lem3  8582  dfac5  8585  dfac2  8587  dfac8  8591  dfac9  8592  dfacacn  8597  dfac13  8598  dfac12r  8602  dfac12k  8603  kmlem2  8607  kmlem13  8618  cdainf  8648  ackbij2  8699  cflim2  8719  isfin4-2  8770  isfin4-3  8771  isf33lem  8822  compsscnv  8827  fin1a2lem6  8861  domtriom  8899  ac9  8939  ac9s  8949  fodomb  8980  brdom3  8982  brdom5  8983  brdom4  8984  brdom7disj  8985  brdom6disj  8986  iunfo  8990  sdomsdomcard  9011  gch2  9126  gch3  9127  eltsk2g  9202  grutsk  9273  grothpw  9277  ordpipq  9393  ltbtwnnq  9429  mappsrpr  9558  map2psrpr  9560  elreal2  9582  le2tri3i  9790  ltadd2iOLD  9792  elnn0nn  10941  elnnnn0b  10943  elnnnn0c  10944  elnnz  10976  elnn0z  10979  elz2  10983  elnnz1  10992  eluz2b2  11260  elnn1uz2  11264  elioo4g  11724  eluzfz2b  11837  fzn0  11842  elfz1end  11858  fzass4  11865  elfz1b  11893  nn0fz0  11919  fzolb  11957  fzon0  11968  elfzo0  11987  fzo1fzo0n0  11988  elfzo0z  11989  elfzo1  11996  om2uzrani  12198  nn0opthi  12488  hashkf  12549  isfinite4  12575  hashprb  12606  hashf1  12653  elss2prb  12676  iswrdb  12710  wrdexb  12716  0wrd0  12729  cotr2g  13089  trclun  13127  sqr0lem  13353  rexanuz  13457  rexuz3  13460  fsum0diag  13887  fprod0diag  14089  sadcp1  14478  isprm6  14715  4sqlem4  14945  mreunirn  15556  isdrs2  16233  isacs5  16467  isacs4  16468  isacs3  16469  isnsg3  16900  gicer  16989  oppgmndb  17055  oppggrpb  17058  pmtrfb  17155  invghm  17523  opprringb  17909  isnzr2hash  18537  abvn0b  18575  gzrngunit  19082  dvdsrzring  19101  zringunit  19111  zlmlmod  19143  zlmassa  19144  cygth  19191  frgpcyg  19193  tgclb  20035  iscldtop  20160  isnrm2  20423  isnrm3  20424  discmp  20462  dfcon2  20483  2ndcsb  20513  dis2ndc  20524  loclly  20551  unisngl  20591  locfindis  20594  iskgen2  20612  dfac14  20682  kqtop  20809  kqt0  20810  kqreg  20815  kqnrm  20816  hmpher  20848  hmphsymb  20850  hmph0  20859  kqhmph  20883  ist1-5lem  20884  elmptrab2  20892  isfil2  20920  filunirn  20946  isufil2  20972  hausflim  21045  isfcls  21073  alexsubALT  21115  istgp2  21155  ustbas  21291  xmetunirn  21401  dscmet  21636  dscopn  21637  isngp4  21674  zcld  21880  zlmclm  22175  iscmet2  22313  iundisj  22550  i1f1lem  22696  fta1b  23169  elply2  23199  elqaa  23327  aannenlem2  23334  wilth  24045  lgsne0  24310  2sqlem2  24341  ostth  24526  mptelee  24974  uhgra0v  25086  wrdumgra  25092  usgra0v  25147  uvtx01vtx  25269  wlkcpr  25306  isspthonpth  25363  eclclwwlkn1  25609  usg2spthonot1  25667  clwlknclwlkdifs  25737  frgra0v  25770  nmlno0lem  26483  isblo3i  26491  blocni  26495  hvsubeq0i  26765  hvaddcani  26767  bcseqi  26822  isch3  26943  norm1exi  26952  hhsssh  26969  shslubi  27087  dfch2  27109  pjoc1i  27133  pjchi  27134  shs00i  27152  chsscon3i  27163  chlejb1i  27178  chj00i  27189  shjshseli  27195  h1de2ctlem  27257  spanunsni  27281  cmcmi  27294  cmbr3i  27302  cmbr4i  27303  pj11i  27413  hosubeq0i  27528  dmadjrnb  27608  nmlnop0iALT  27697  lnopeq0i  27709  elunop2  27715  lnconi  27735  lncnopbd  27739  adjbdlnb  27786  adjbd1o  27787  adjeq0  27793  rnbra  27809  pjss1coi  27865  pjss2coi  27866  pjnormssi  27870  pjssdif2i  27876  pjssdif1i  27877  dfpjop  27884  pjinvari  27893  pjin2i  27895  pjci  27902  pjcmul1i  27903  pjcmul2i  27904  strb  27960  hstrbi  27968  mdsl1i  28023  atom1d  28055  chrelat2i  28067  cvbr4i  28069  cvexchi  28071  sumdmdi  28122  dmdbr4ati  28123  dmdbr5ati  28124  dmdbr6ati  28125  dmdbr7ati  28126  cdj3i  28143  difeq  28200  iundisjf  28248  cnvoprab  28357  fpwrelmap  28367  iundisjfi  28421  xrge0tsmsbi  28598  issgon  28994  measbasedom  29073  oddpwdc  29236  eulerpartlemt  29253  ballotlem2  29370  ballotlemrinv  29415  ballotlemrinvOLD  29453  bnj1533  29712  bnj983  29811  elmsta  30235  nepss  30399  dfpo2  30444  dfon2  30487  distel  30499  elno2  30590  bdayfo  30613  fnimage  30745  altopthsn  30777  ellines  30968  rankeq1o  30987  opnrebl2  31026  df3nandALT1  31106  pm4.81ALT  31178  bj-dfbi6  31196  bj-consensus  31201  bj-falor2  31214  bj-bibibi  31215  bj-andnotim  31217  bj-ssbeq  31285  bj-ssb0  31286  bj-19.41al  31295  bj-sb56  31297  bj-cbvexw  31318  bj-equs45fv  31408  bj-sb6  31425  bj-axext4  31430  bj-hbaeb2  31465  bj-hbnaeb  31467  bj-equsal  31473  bj-mo3OLD  31492  bj-cleqhyp  31544  bj-csbsnlem  31550  bj-snsetex  31602  bj-snglex  31612  bj-1uplth  31646  bj-1uplex  31647  bj-2uplth  31660  bj-2uplex  31661  bj-elid  31685  bj-elid3  31687  bj-eldiag2  31692  mptsnunlem  31785  topdifinf  31797  elxp8  31819  finxp1o  31829  wl-nfnbi  31904  wl-exeq  31912  wl-aleq  31913  wl-nfeqfb  31915  wl-ax11-lem6  31965  volsupnfl  32030  dvtanlemOLD  32036  cover2  32085  isbnd3  32161  cntotbnd  32173  heibor  32198  isfld2  32283  isfldidl  32346  orfa  32360  prtlem16  32486  isltrn2N  33730  ismrc  35588  isnacs3  35597  rexzrexnn0  35692  eldioph4b  35699  dford3  35928  wopprc  35930  ttac  35936  pw2f1ocnv  35937  dfac11  35965  dfac21  35969  isnumbasabl  36010  isnumbasgrp  36011  dfacbasgrp  36012  aaitgo  36073  ifpbi1b  36192  rp-fakeimass  36201  rp-fakeanorass  36202  rp-fakenanass  36204  rp-isfinite5  36207  rp-isfinite6  36208  rtrclex  36269  cnvtrrel  36307  rp-imass  36411  frege54cor0a  36504  nanorxor  36697  nzss  36710  pm10.55  36762  pm11.57  36783  sbeqalbi  36795  pm13.192  36805  pm13.194  36807  ipo0  36846  ifr0  36847  xpexb  36851  3impexpbicom  36878  com3rgbi  36915  pm2.43bgbi  36918  pm2.43cbi  36919  sb5ALT  36926  trsbc  36945  2pm13.193  36963  ax6e2ndeq  36970  2uasbanh  36972  eelT01  37136  eel0T1  37137  uunT1  37207  zfregs2VD  37277  equncomVD  37305  trsbcVD  37314  undif3VD  37319  2pm13.193VD  37340  ax6e2eqVD  37344  ax6e2ndeqVD  37346  2uasbanhVD  37348  ax6e2ndeqALT  37368  fompt  37505  elfzfzo  37524  dvnprodlem3  37861  elaa2  38137  sge00  38256  ismea  38327  elhoi  38402  ovn0  38426  confun  38565  reuan  38639  afvfv0bi  38692  ffnafv  38711  clel5  39021  propeqop  39039  funop  39061  funsneqopb  39067  residfi  39081  wrdupgr  39224  wrdumgr  39234  uspgrupgrushgr  39312  usgrumgruspgr  39315  usgruspgrb  39316  uvtxa01vtx0  39519  umgrislfupgr  39719  usgrislfuspgr  39720  isclWlkb  39800  mgm2mgm  40136  isringrng  40154  nnpw2pb  40671