MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbii Unicode version

Theorem impbii 181
Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
impbii.1  |-  ( ph  ->  ps )
impbii.2  |-  ( ps 
->  ph )
Assertion
Ref Expression
impbii  |-  ( ph  <->  ps )

Proof of Theorem impbii
StepHypRef Expression
1 impbii.1 . 2  |-  ( ph  ->  ps )
2 impbii.2 . 2  |-  ( ps 
->  ph )
3 bi3 180 . 2  |-  ( (
ph  ->  ps )  -> 
( ( ps  ->  ph )  ->  ( ph  <->  ps ) ) )
41, 2, 3mp2 9 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  dfbi1  185  bicom  192  biid  228  2th  231  pm5.74  236  bitri  241  notnot  283  con34b  284  notbi  287  bibi2i  305  con1b  324  con2b  325  bi2.04  351  pm5.4  352  imdi  353  pm4.8  355  pm4.81  356  orcom  377  dfor2  401  impexp  434  ancom  438  oridm  501  orbi2i  506  or12  510  pm4.45im  546  pm4.44  561  pm4.79  567  anass  631  jaob  759  jcab  834  andi  838  pm4.72  847  oibabs  852  pm4.82  895  consensus  926  rnlem  932  3jaob  1246  truan  1337  dfnot  1338  3impexp  1372  3impexpbicom  1373  cad1  1404  tbw-bijust  1469  tbw-negdf  1470  19.26  1600  sbbii  1660  19.9v  1671  equcom  1687  ax12b  1696  19.3vOLD  1703  cbvalw  1708  cbvalvw  1709  alcom  1744  19.9hOLD  1789  19.3  1793  19.23hOLD  1829  equsalhwOLD  1851  19.21hOLD  1852  excomOLD  1871  19.41  1889  19.41OLD  1890  equsalOLD  1955  equsex  1957  ax12olem1  1960  ax12olem1OLD  1965  ax12olem3OLD  1967  cbval  2019  equs45f  2024  equvin  2035  sb6f  2072  dfsb2  2088  sbn  2095  sbim  2098  sb5rf  2123  sb6rf  2124  sb9  2128  mo  2260  eu2  2263  mo2  2267  exmoeu  2280  euan  2295  2mo  2316  2eu6  2323  axext4  2371  cleqh  2484  nebi  2621  r19.26  2781  ralcom3  2816  ceqsex  2933  gencbvex  2941  gencbvex2  2942  eqvinc  3006  pm13.183  3019  rr19.3v  3020  rr19.28v  3021  euxfr2  3062  reu6  3066  reu3  3067  sbnfc2  3252  sspss  3389  unineq  3534  uneqin  3535  undif3  3545  difrab  3558  un00  3606  ssdifeq0  3653  r19.2zb  3661  ralf0  3677  elpr2  3776  snidb  3783  tppreqb  3882  difsnb  3883  pwpw0  3889  sssn  3900  preq12b  3916  preqsn  3922  pwsnALT  3952  unissint  4016  uniintsn  4029  iununi  4116  intex  4297  intnex  4298  iin0  4314  axpweq  4317  nfcvb  4335  sspwb  4354  unipw  4355  opnz  4373  opth  4376  opthwiener  4399  ssopab2b  4422  pwssun  4430  elon2  4533  unexb  4649  eusvnfb  4659  eusv2nf  4661  ralxfrALT  4682  uniexb  4692  iunpw  4699  ordeleqon  4709  onintrab  4721  unon  4751  onuninsuci  4760  ordzsl  4765  onzsl  4766  opelxp  4848  opthprc  4865  relop  4963  issetid  4967  xpid11  5031  elres  5121  iss  5129  issref  5187  asymref2  5191  xpnz  5232  ssrnres  5249  dfrel2  5261  relrelss  5333  unixp0  5343  fn0  5504  funssxp  5544  f00  5568  dffo2  5597  ffoss  5647  f1o00  5650  fo00  5651  fv3  5684  dffn5  5711  dff2  5820  dff3  5821  dffo4  5824  dffo5  5825  exfo  5826  fmpt  5829  ffnfv  5833  fsn  5845  fsn2  5847  fconstfv  5893  isores1  5993  ssoprab2b  6070  eqfnov2  6116  1st2ndb  6326  reldmtpos  6423  riotaundb  6527  abianfp  6652  omopthi  6836  mapsn  6991  mapsncnv  6996  mptelixpg  7035  elixpsn  7037  ixpsnf1o  7038  bren2  7074  en0  7106  en1  7110  en1b  7111  sbthb  7164  canth2  7196  onfin2  7234  sdom1  7244  1sdom  7247  fineqv  7260  unfilem1  7307  fiint  7319  pwfi  7337  unifpw  7344  wofib  7447  sucprcreg  7500  opthreg  7506  suc11reg  7507  infeq5  7525  rankwflemb  7652  r1elss  7665  pwwf  7666  unwf  7669  uniwf  7678  rankonid  7688  rankr1id  7721  rankuni  7722  rankxplim3  7738  scott0  7743  karden  7752  isnum3  7774  oncard  7780  card1  7788  cardlim  7792  cardmin2  7818  pm54.43lem  7819  ween  7849  acnnum  7866  alephsuc2  7894  alephgeom  7896  iscard3  7907  dfac3  7935  dfac4  7936  dfac5lem3  7939  dfac5  7942  dfac2  7944  dfac8  7948  dfac9  7949  dfacacn  7954  dfac13  7955  dfac12r  7959  dfac12k  7960  kmlem2  7964  kmlem13  7975  cdainf  8005  ackbij2  8056  cflim2  8076  isfin4-2  8127  isfin4-3  8128  isf33lem  8179  compsscnv  8184  fin1a2lem6  8218  domtriom  8256  ac9  8296  ac9s  8306  fodomb  8337  brdom3  8339  brdom5  8340  brdom4  8341  brdom7disj  8342  brdom6disj  8343  iunfo  8347  sdomsdomcard  8368  gch2  8487  gch3  8488  eltsk2g  8559  grutsk  8630  grothpw  8634  ordpipq  8752  ltbtwnnq  8788  mappsrpr  8916  map2psrpr  8918  elreal2  8940  le2tri3i  9135  ltadd2i  9136  elnn0nn  10194  elnnnn0b  10196  elnnnn0c  10197  elnnz  10224  elnn0z  10226  elz2  10230  elnnz1  10239  eluz2b2  10480  elnn1uz2  10484  elioo4g  10903  eluzfz2b  10998  fzn0  11002  elfz1end  11013  fzass4  11022  fzolb  11075  fzon0  11086  elfzo0  11101  om2uzrani  11219  nn0opthi  11490  hashkf  11547  hashprb  11595  hashf1  11633  wrdexb  11690  sqr0lem  11973  rexanuz  12076  rexuz3  12079  fsum0diag  12488  sadcp1  12894  isprm6  13036  4sqlem4  13247  mreunirn  13753  isdrs2  14323  isacs5  14525  isacs4  14526  isacs3  14527  isnsg3  14901  gicer  14990  oppgmndb  15078  oppggrpb  15081  invghm  15380  opprrngb  15664  abvn0b  16289  gzrngunit  16687  zrngunit  16688  dvdsrz  16690  zlmlmod  16727  zlmassa  16728  cygth  16775  frgpcyg  16777  tgclb  16958  iscldtop  17082  isnrm2  17344  isnrm3  17345  discmp  17383  dfcon2  17403  2ndcsb  17433  dis2ndc  17444  loclly  17471  iskgen2  17501  dfac14  17571  kqtop  17698  kqt0  17699  kqreg  17704  kqnrm  17705  hmpher  17737  hmphsymb  17739  hmph0  17748  kqhmph  17772  ist1-5lem  17773  elmptrab2  17781  isfil2  17809  filunirn  17835  isufil2  17861  hausflim  17934  isfcls  17962  alexsubALT  18003  istgp2  18042  ustbas  18178  xmetunirn  18276  dscmet  18491  dscopn  18492  isngp4  18529  zcld  18715  zlmclm  18991  iscmet2  19118  iundisj  19309  i1f1lem  19448  fta1b  19959  elply2  19982  elqaa  20106  aannenlem2  20113  wilth  20721  lgsne0  20984  2sqlem2  21015  ostth  21200  uhgra0v  21212  wrdumgra  21218  usgra0v  21258  uvtx01vtx  21367  istrl2  21402  nmlno0lem  22142  isblo3i  22150  blocni  22154  hvsubeq0i  22413  hvaddcani  22415  bcseqi  22470  isch3  22592  norm1exi  22600  hhsssh  22617  shslubi  22735  dfch2  22757  pjoc1i  22781  pjchi  22782  shs00i  22800  chsscon3i  22811  chlejb1i  22826  chj00i  22837  shjshseli  22843  h1de2ctlem  22905  spanunsni  22929  cmcmi  22942  cmbr3i  22950  cmbr4i  22951  pj11i  23061  hosubeq0i  23177  dmadjrnb  23257  nmlnop0iALT  23346  lnopeq0i  23358  elunop2  23364  lnconi  23384  lncnopbd  23388  adjbdlnb  23435  adjbd1o  23436  adjeq0  23442  rnbra  23458  pjss1coi  23514  pjss2coi  23515  pjnormssi  23519  pjssdif2i  23525  pjssdif1i  23526  dfpjop  23533  pjinvari  23542  pjin2i  23544  pjci  23551  pjcmul1i  23552  pjcmul2i  23553  strb  23609  hstrbi  23617  mdsl1i  23672  atom1d  23704  chrelat2i  23716  cvbr4i  23718  cvexchi  23720  sumdmdi  23771  dmdbr4ati  23772  dmdbr5ati  23773  dmdbr6ati  23774  dmdbr7ati  23775  cdj3i  23792  difeq  23842  iundisjf  23872  elfzo1  23989  iundisjfi  23990  xrge0tsmsbi  24053  issgon  24302  measbasedom  24351  ballotlem2  24525  ballotlemrinv  24570  nepss  24954  dfpo2  25136  dfon2  25172  distel  25184  elno2  25332  bdayfo  25353  elfix  25467  dffix2  25469  fnimage  25492  altopthsn  25520  mptelee  25548  ellines  25800  rankeq1o  25826  df3nandALT1  25860  wl-pm5.74lem  25941  volsupnfl  25956  opnrebl2  26015  locfindis  26076  cover2  26106  isbnd3  26184  cntotbnd  26196  heibor  26221  isfld2  26306  isfldidl  26369  prtlem16  26409  funsnfsup  26434  ismrc  26446  isnacs3  26455  rexzrexnn0  26555  eldioph4b  26563  dford3  26790  wopprc  26792  ttac  26798  pw2f1ocnv  26799  dfac11  26829  dfac21  26833  isnumbasabl  26940  isnumbasgrp  26941  dfacbasgrp  26942  aaitgo  27036  pmtrfb  27075  pm10.55  27233  pm11.57  27257  sbeqalbi  27269  pm13.192  27279  pm13.194  27281  ipo0  27320  ifr0  27321  xpexb  27326  reuan  27626  afvfv0bi  27685  ffnafv  27704  frgra0v  27746  com3rgbi  27940  pm2.43bgbi  27943  pm2.43cbi  27944  sb5ALT  27952  trsbc  27968  2pm13.193  27982  a9e2ndeq  27989  2uasbanh  27991  eelT01  28159  eel0T1  28160  uunT1  28233  zfregs2VD  28294  equncomVD  28321  trsbcVD  28330  undif3VD  28335  2pm13.193VD  28356  a9e2eqVD  28360  a9e2ndeqVD  28362  2uasbanhVD  28364  a9e2ndeqALT  28385  bnj1533  28561  bnj983  28660  alcomwAUX7  28782  ax12olem3aAUX7  28795  equsalNEW7  28825  cbvalwwAUX7  28855  equvinNEW7  28865  sbnNEW7  28898  sbimNEW7  28901  sb5rfNEW7  28924  sb6rfNEW7  28925  sb8wAUX7  28926  equs45fNEW7  28954  sb6fNEW7  28966  dfsb2NEW7  28971  alcomw9bAUX7  28993  alcomOLD7  28997  excomOLD7  29010  cbvalOLD7  29041  nfsb4tw2AUXOLD7  29062  sbcomOLD7  29071  sb8OLD7  29072  sb9iOLD7  29074  sb9OLD7  29075  isltrn2N  30234
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator