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  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  446  ancom  450  oridm  514  orbi2i  519  or12  523  pm4.45im  562  pm4.44  577  pm4.79  583  anass  649  jaob  783  jcab  863  andi  867  pm4.72  876  oibabs  881  pm4.82  928  consensus  959  rnlemOLD  965  cases2  971  cases2OLD  972  3jaob  1291  truanOLD  1401  dfnotOLD  1403  cad1  1453  tbw-bijust  1518  tbw-negdf  1519  19.26  1667  19.35  1674  19.21v  1716  sbbii  1733  19.9v  1741  19.23v  1747  19.41v  1757  equcom  1780  equvin  1790  cbvalw  1794  alcom  1831  19.3  1874  19.41  1957  cbval  2007  equsex  2024  aecom  2037  equvinOLD  2076  equs45f  2077  dfsb2  2100  sb6f  2112  sbim  2122  sb6  2159  mo2v  2275  mo2vOLD  2276  mo2vOLDOLD  2277  exmoeu  2302  mo3  2309  mo3OLD  2310  mo2OLD  2320  moanim  2336  euan  2337  2mo  2359  2moOLD  2360  2eu6  2369  2eu6OLD  2370  axext4  2425  eqcom  2452  cleqhOLD  2559  nebi  2753  r19.26  2970  ralcom3  3009  ceqsex  3131  gencbvex  3139  gencbvex2  3140  eqvinc  3212  pm13.183  3226  rr19.3v  3227  rr19.28v  3228  euxfr2  3270  reu6  3274  reu3  3275  sspss  3588  unineq  3733  uneqin  3734  undif3  3744  difrab  3757  sbnfc2  3840  un00  3848  ssdifeq0  3896  r19.2zb  3905  ralf0  3921  elpr2  4033  snidb  4041  rabsnifsb  4083  tppreqb  4156  difsnb  4157  pwpw0  4163  sssn  4173  preq12b  4191  preqsn  4198  pwsnALT  4229  unissint  4296  uniintsn  4309  iununi  4400  intex  4593  intnex  4594  iin0  4611  axpweq  4614  eusvnfb  4633  eusv2nf  4635  ralxfrALT  4656  nfcvb  4667  sspwb  4686  unipw  4687  opnz  4708  opth  4711  opthwiener  4739  ssopab2b  4764  pwssun  4776  elon2  4879  opelxp  5019  opthprc  5037  relop  5143  issetid  5147  xpid11  5214  elres  5299  eldmeldmressn  5304  iss  5311  restidsing  5320  issref  5370  asymref2  5374  xpnz  5416  xpdifid  5425  ssrnres  5435  dfrel2  5447  relrelss  5521  unixp0  5531  fn0  5690  funssxp  5734  f00  5757  f0bi  5758  dffo2  5789  f1o00  5838  fo00  5839  fv3  5869  dffn5  5903  dff2  6028  dff3  6029  dffo4  6032  dffo5  6033  exfo  6034  fmpt  6037  ffnfv  6042  fsn  6054  fsn2  6056  fnsnb  6075  fconstfvOLD  6119  isores1  6215  ssoprab2b  6339  eqfnov2  6394  unexb  6585  uniexb  6595  iunpw  6599  ordeleqon  6609  onintrab  6621  unon  6651  onuninsuci  6660  ordzsl  6665  onzsl  6666  f1oexbi  6735  ffoss  6746  1st2ndb  6823  suppssov1  6934  suppssfv  6938  reldmtpos  6965  omopthi  7308  mapsn  7462  mapsncnv  7467  mptelixpg  7508  elixpsn  7510  ixpsnf1o  7511  bren2  7548  en0  7580  en1  7584  en1b  7585  sbthb  7640  canth2  7672  onfin2  7711  sdom1  7721  1sdom  7724  fineqv  7737  unfilem1  7786  fiint  7799  pwfi  7817  unifpw  7825  wofib  7973  sucprcreg  8028  sucprcregOLD  8029  opthreg  8038  suc11reg  8039  infeq5  8057  rankwflemb  8214  r1elss  8227  pwwf  8228  unwf  8231  uniwf  8240  rankonid  8250  rankr1id  8283  rankuni  8284  rankxplim3  8302  scott0  8307  karden  8316  isnum3  8338  oncard  8344  card1  8352  cardlim  8356  cardmin2  8382  pm54.43lem  8383  ween  8419  acnnum  8436  alephsuc2  8464  alephgeom  8466  iscard3  8477  dfac3  8505  dfac4  8506  dfac5lem3  8509  dfac5  8512  dfac2  8514  dfac8  8518  dfac9  8519  dfacacn  8524  dfac13  8525  dfac12r  8529  dfac12k  8530  kmlem2  8534  kmlem13  8545  cdainf  8575  ackbij2  8626  cflim2  8646  isfin4-2  8697  isfin4-3  8698  isf33lem  8749  compsscnv  8754  fin1a2lem6  8788  domtriom  8826  ac9  8866  ac9s  8876  fodomb  8907  brdom3  8909  brdom5  8910  brdom4  8911  brdom7disj  8912  brdom6disj  8913  iunfo  8917  sdomsdomcard  8938  gch2  9056  gch3  9057  eltsk2g  9132  grutsk  9203  grothpw  9207  ordpipq  9323  ltbtwnnq  9359  mappsrpr  9488  map2psrpr  9490  elreal2  9512  le2tri3i  9717  ltadd2iOLD  9719  elnn0nn  10845  elnnnn0b  10847  elnnnn0c  10848  elnnz  10881  elnn0z  10884  elz2  10888  elnnz1  10897  eluz2b2  11165  elnn1uz2  11169  elioo4g  11596  eluzfz2b  11706  fzn0  11711  elfz1end  11726  fzass4  11732  elfz1b  11759  nn0fz0  11785  fzolb  11816  fzon0  11827  elfzo0  11845  fzo1fzo0n0  11846  elfzo0z  11847  elfzo1  11853  om2uzrani  12045  nn0opthi  12332  hashkf  12389  hashprb  12444  hashf1  12488  iswrdbi  12536  wrdexb  12540  0wrd0  12548  sqr0lem  13056  rexanuz  13160  rexuz3  13163  fsum0diag  13574  fprod0diag  13772  sadcp1  14087  isprm6  14232  4sqlem4  14452  mreunirn  14980  isdrs2  15547  isacs5  15781  isacs4  15782  isacs3  15783  isnsg3  16214  gicer  16303  oppgmndb  16369  oppggrpb  16372  pmtrfb  16469  invghm  16821  opprringb  17260  isnzr2hash  17891  abvn0b  17930  funsnfsupOLD  18235  gzrngunit  18462  dvdsrzring  18485  dvdsrz  18486  zringunit  18498  zrngunit  18499  zlmlmod  18538  zlmassa  18539  cygth  18588  frgpcyg  18590  tgclb  19450  iscldtop  19574  isnrm2  19837  isnrm3  19838  discmp  19876  dfcon2  19898  2ndcsb  19928  dis2ndc  19939  loclly  19966  unisngl  20006  locfindis  20009  iskgen2  20027  dfac14  20097  kqtop  20224  kqt0  20225  kqreg  20230  kqnrm  20231  hmpher  20263  hmphsymb  20265  hmph0  20274  kqhmph  20298  ist1-5lem  20299  elmptrab2  20307  isfil2  20335  filunirn  20361  isufil2  20387  hausflim  20460  isfcls  20488  alexsubALT  20529  istgp2  20568  ustbas  20708  xmetunirn  20818  dscmet  21071  dscopn  21072  isngp4  21109  zcld  21296  zlmclm  21573  iscmet2  21711  iundisj  21936  i1f1lem  22074  fta1b  22548  elply2  22571  elqaa  22696  aannenlem2  22703  wilth  23323  lgsne0  23586  2sqlem2  23617  ostth  23802  mptelee  24176  uhgra0v  24288  wrdumgra  24294  usgra0v  24349  uvtx01vtx  24470  wlkcpr  24507  isspthonpth  24564  eclclwwlkn1  24810  usg2spthonot1  24868  clwlknclwlkdifs  24938  frgra0v  24971  nmlno0lem  25686  isblo3i  25694  blocni  25698  hvsubeq0i  25958  hvaddcani  25960  bcseqi  26015  isch3  26137  norm1exi  26146  hhsssh  26163  shslubi  26281  dfch2  26303  pjoc1i  26327  pjchi  26328  shs00i  26346  chsscon3i  26357  chlejb1i  26372  chj00i  26383  shjshseli  26389  h1de2ctlem  26451  spanunsni  26475  cmcmi  26488  cmbr3i  26496  cmbr4i  26497  pj11i  26607  hosubeq0i  26723  dmadjrnb  26803  nmlnop0iALT  26892  lnopeq0i  26904  elunop2  26910  lnconi  26930  lncnopbd  26934  adjbdlnb  26981  adjbd1o  26982  adjeq0  26988  rnbra  27004  pjss1coi  27060  pjss2coi  27061  pjnormssi  27065  pjssdif2i  27071  pjssdif1i  27072  dfpjop  27079  pjinvari  27088  pjin2i  27090  pjci  27097  pjcmul1i  27098  pjcmul2i  27099  strb  27155  hstrbi  27163  mdsl1i  27218  atom1d  27250  chrelat2i  27262  cvbr4i  27264  cvexchi  27266  sumdmdi  27317  dmdbr4ati  27318  dmdbr5ati  27319  dmdbr6ati  27320  dmdbr7ati  27321  cdj3i  27338  difeq  27394  iundisjf  27426  cnvoprab  27524  fpwrelmap  27534  iundisjfi  27579  xrge0tsmsbi  27754  issgon  28101  measbasedom  28151  oddpwdc  28271  eulerpartlemt  28288  ballotlem2  28405  ballotlemrinv  28450  elmsta  28886  nepss  29073  dfpo2  29160  dfon2  29200  distel  29212  elno2  29390  bdayfo  29411  fnimage  29555  altopthsn  29587  ellines  29778  rankeq1o  29804  df3nandALT1  29838  wl-nfnbi  29955  wl-exeq  29963  wl-aleq  29964  wl-nfeqfb  29966  wl-ax11-lem6  30006  volsupnfl  30035  dvtanlem  30040  opnrebl2  30115  cover2  30180  isbnd3  30256  cntotbnd  30268  heibor  30293  isfld2  30378  isfldidl  30441  orfa  30455  prtlem16  30586  ismrc  30609  isnacs3  30618  rexzrexnn0  30713  eldioph4b  30721  dford3  30946  wopprc  30948  ttac  30954  pw2f1ocnv  30955  dfac11  30984  dfac21  30988  isnumbasabl  31031  isnumbasgrp  31032  dfacbasgrp  31033  aaitgo  31087  nanorxor  31161  nzss  31198  pm10.55  31228  pm11.57  31249  sbeqalbi  31261  pm13.192  31271  pm13.194  31273  ipo0  31312  ifr0  31313  xpexb  31317  elfzfzo  31412  dvnprodlem3  31699  elaa2  31971  reuan  32139  afvfv0bi  32191  ffnafv  32210  residfi  32268  mgm2mgm  32504  isringrng  32525  3impexp  33088  3impexpbicom  33089  com3rgbi  33152  pm2.43bgbi  33155  pm2.43cbi  33156  sb5ALT  33163  trsbc  33179  2pm13.193  33193  ax6e2ndeq  33200  2uasbanh  33202  eelT01  33371  eel0T1  33372  uunT1  33445  zfregs2VD  33509  equncomVD  33536  trsbcVD  33545  undif3VD  33550  2pm13.193VD  33571  ax6e2eqVD  33575  ax6e2ndeqVD  33577  2uasbanhVD  33579  ax6e2ndeqALT  33599  bnj1533  33778  bnj983  33877  pm4.81ALT  34004  bj-dfbi6  34024  bj-dfif5ALT  34032  bj-consensus  34045  bj-falor2  34057  bj-bibibi  34058  bj-andnotim  34060  bj-cbvexw  34118  bj-cbvalv  34179  bj-equsexv  34195  bj-equsexvv  34196  bj-equs45fv  34214  bj-sb6  34233  bj-axext4  34238  bj-cleqh  34241  bj-hbaeb2  34274  bj-hbnaeb  34276  bj-equsal  34282  bj-dfcleq  34349  bj-csbsnlem  34353  bj-snsetex  34404  bj-snglex  34414  bj-1uplth  34448  bj-1uplex  34449  bj-2uplth  34462  bj-2uplex  34463  bj-elid  34474  bj-elid3  34476  bj-eldiag2  34482  isltrn2N  35719  rp-fakeimass  37574  rp-fakeanorass  37575  rp-fakenanass  37577  rp-isfinite4  37580  rp-isfinite5  37581  rp-isfinite6  37582  cnvtrrel  37610  cotr2g  37614  rp-imass  37617  bj-frege54cor0a  37710