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  1661  19.9v  1672  equcom  1688  19.3vOLD  1705  cbvalw  1710  cbvalvwOLD  1712  alcom  1748  19.3  1787  19.9hOLD  1791  19.23hOLD  1835  equsalhwOLD  1857  19.21hOLD  1858  excomOLD  1878  19.41  1896  19.41OLD  1897  equsalOLD  1967  equsex  1969  ax12olem1  1972  ax12olem1OLD  1977  ax12olem3OLD  1979  cbval  2040  equs45f  2047  equvin  2055  sb6f  2092  dfsb2  2108  sbn  2115  sbim  2118  sb5rf  2143  sb6rf  2144  sb9  2148  mo  2280  eu2  2283  mo2  2287  exmoeu  2300  euan  2315  2mo  2336  2eu6  2343  axext4  2392  cleqh  2505  nebi  2642  r19.26  2802  ralcom3  2837  ceqsex  2954  gencbvex  2962  gencbvex2  2963  eqvinc  3027  pm13.183  3040  rr19.3v  3041  rr19.28v  3042  euxfr2  3083  reu6  3087  reu3  3088  sbnfc2  3273  sspss  3410  unineq  3555  uneqin  3556  undif3  3566  difrab  3579  un00  3627  ssdifeq0  3674  r19.2zb  3682  ralf0  3698  elpr2  3797  snidb  3804  tppreqb  3903  difsnb  3904  pwpw0  3910  sssn  3921  preq12b  3938  preqsn  3944  pwsnALT  3974  unissint  4038  uniintsn  4051  iununi  4139  intex  4320  intnex  4321  iin0  4337  axpweq  4340  nfcvb  4358  sspwb  4377  unipw  4378  opnz  4396  opth  4399  opthwiener  4422  ssopab2b  4445  pwssun  4453  elon2  4556  unexb  4672  eusvnfb  4682  eusv2nf  4684  ralxfrALT  4705  uniexb  4715  iunpw  4722  ordeleqon  4732  onintrab  4744  unon  4774  onuninsuci  4783  ordzsl  4788  onzsl  4789  opelxp  4871  opthprc  4888  relop  4986  issetid  4990  xpid11  5054  elres  5144  iss  5152  issref  5210  asymref2  5214  xpnz  5255  ssrnres  5272  dfrel2  5284  relrelss  5356  unixp0  5366  fn0  5527  funssxp  5567  f00  5591  dffo2  5620  ffoss  5670  f1o00  5673  fo00  5674  fv3  5707  dffn5  5735  dff2  5844  dff3  5845  dffo4  5848  dffo5  5849  exfo  5850  fmpt  5853  ffnfv  5857  fsn  5869  fsn2  5871  fconstfv  5917  isores1  6017  ssoprab2b  6094  eqfnov2  6140  1st2ndb  6350  reldmtpos  6450  riotaundb  6554  abianfp  6679  omopthi  6863  mapsn  7018  mapsncnv  7023  mptelixpg  7062  elixpsn  7064  ixpsnf1o  7065  bren2  7101  en0  7133  en1  7137  en1b  7138  sbthb  7191  canth2  7223  onfin2  7261  sdom1  7271  1sdom  7274  fineqv  7287  unfilem1  7334  fiint  7346  pwfi  7364  unifpw  7371  wofib  7474  sucprcreg  7527  opthreg  7533  suc11reg  7534  infeq5  7552  rankwflemb  7679  r1elss  7692  pwwf  7693  unwf  7696  uniwf  7705  rankonid  7715  rankr1id  7748  rankuni  7749  rankxplim3  7765  scott0  7770  karden  7779  isnum3  7801  oncard  7807  card1  7815  cardlim  7819  cardmin2  7845  pm54.43lem  7846  ween  7876  acnnum  7893  alephsuc2  7921  alephgeom  7923  iscard3  7934  dfac3  7962  dfac4  7963  dfac5lem3  7966  dfac5  7969  dfac2  7971  dfac8  7975  dfac9  7976  dfacacn  7981  dfac13  7982  dfac12r  7986  dfac12k  7987  kmlem2  7991  kmlem13  8002  cdainf  8032  ackbij2  8083  cflim2  8103  isfin4-2  8154  isfin4-3  8155  isf33lem  8206  compsscnv  8211  fin1a2lem6  8245  domtriom  8283  ac9  8323  ac9s  8333  fodomb  8364  brdom3  8366  brdom5  8367  brdom4  8368  brdom7disj  8369  brdom6disj  8370  iunfo  8374  sdomsdomcard  8395  gch2  8514  gch3  8515  eltsk2g  8586  grutsk  8657  grothpw  8661  ordpipq  8779  ltbtwnnq  8815  mappsrpr  8943  map2psrpr  8945  elreal2  8967  le2tri3i  9163  ltadd2i  9164  elnn0nn  10222  elnnnn0b  10224  elnnnn0c  10225  elnnz  10252  elnn0z  10254  elz2  10258  elnnz1  10267  eluz2b2  10508  elnn1uz2  10512  elioo4g  10931  eluzfz2b  11026  fzn0  11030  elfz1end  11041  fzass4  11050  fzolb  11104  fzon0  11115  elfzo0  11130  elfzo1  11132  om2uzrani  11251  nn0opthi  11522  hashkf  11579  hashprb  11627  hashf1  11665  wrdexb  11722  sqr0lem  12005  rexanuz  12108  rexuz3  12111  fsum0diag  12520  sadcp1  12926  isprm6  13068  4sqlem4  13279  mreunirn  13785  isdrs2  14355  isacs5  14557  isacs4  14558  isacs3  14559  isnsg3  14933  gicer  15022  oppgmndb  15110  oppggrpb  15113  invghm  15412  opprrngb  15696  abvn0b  16321  gzrngunit  16723  zrngunit  16724  dvdsrz  16726  zlmlmod  16763  zlmassa  16764  cygth  16811  frgpcyg  16813  tgclb  16994  iscldtop  17118  isnrm2  17380  isnrm3  17381  discmp  17419  dfcon2  17439  2ndcsb  17469  dis2ndc  17480  loclly  17507  iskgen2  17537  dfac14  17607  kqtop  17734  kqt0  17735  kqreg  17740  kqnrm  17741  hmpher  17773  hmphsymb  17775  hmph0  17784  kqhmph  17808  ist1-5lem  17809  elmptrab2  17817  isfil2  17845  filunirn  17871  isufil2  17897  hausflim  17970  isfcls  17998  alexsubALT  18039  istgp2  18078  ustbas  18214  xmetunirn  18324  dscmet  18577  dscopn  18578  isngp4  18615  zcld  18801  zlmclm  19077  iscmet2  19204  iundisj  19399  i1f1lem  19538  fta1b  20049  elply2  20072  elqaa  20196  aannenlem2  20203  wilth  20811  lgsne0  21074  2sqlem2  21105  ostth  21290  uhgra0v  21302  wrdumgra  21308  usgra0v  21348  uvtx01vtx  21458  istrl2  21495  isspthonpth  21541  nmlno0lem  22251  isblo3i  22259  blocni  22263  hvsubeq0i  22522  hvaddcani  22524  bcseqi  22579  isch3  22701  norm1exi  22709  hhsssh  22726  shslubi  22844  dfch2  22866  pjoc1i  22890  pjchi  22891  shs00i  22909  chsscon3i  22920  chlejb1i  22935  chj00i  22946  shjshseli  22952  h1de2ctlem  23014  spanunsni  23038  cmcmi  23051  cmbr3i  23059  cmbr4i  23060  pj11i  23170  hosubeq0i  23286  dmadjrnb  23366  nmlnop0iALT  23455  lnopeq0i  23467  elunop2  23473  lnconi  23493  lncnopbd  23497  adjbdlnb  23544  adjbd1o  23545  adjeq0  23551  rnbra  23567  pjss1coi  23623  pjss2coi  23624  pjnormssi  23628  pjssdif2i  23634  pjssdif1i  23635  dfpjop  23642  pjinvari  23651  pjin2i  23653  pjci  23660  pjcmul1i  23661  pjcmul2i  23662  strb  23718  hstrbi  23726  mdsl1i  23781  atom1d  23813  chrelat2i  23825  cvbr4i  23827  cvexchi  23829  sumdmdi  23880  dmdbr4ati  23881  dmdbr5ati  23882  dmdbr6ati  23883  dmdbr7ati  23884  cdj3i  23901  difeq  23955  iundisjf  23986  iundisjfi  24109  xrge0tsmsbi  24181  issgon  24463  measbasedom  24513  ballotlem2  24703  ballotlemrinv  24748  nepss  25132  fprod0diag  25267  dfpo2  25330  dfon2  25366  distel  25378  elno2  25526  bdayfo  25547  elfix  25661  dffix2  25663  fnimage  25686  altopthsn  25714  mptelee  25742  ellines  25994  rankeq1o  26020  df3nandALT1  26054  wl-pm5.74lem  26135  volsupnfl  26154  opnrebl2  26218  locfindis  26279  cover2  26309  isbnd3  26387  cntotbnd  26399  heibor  26424  isfld2  26509  isfldidl  26572  prtlem16  26612  funsnfsup  26637  ismrc  26649  isnacs3  26658  rexzrexnn0  26758  eldioph4b  26766  dford3  26993  wopprc  26995  ttac  27001  pw2f1ocnv  27002  dfac11  27032  dfac21  27036  isnumbasabl  27143  isnumbasgrp  27144  dfacbasgrp  27145  aaitgo  27239  pmtrfb  27278  pm10.55  27436  pm11.57  27460  sbeqalbi  27472  pm13.192  27482  pm13.194  27484  ipo0  27523  ifr0  27524  xpexb  27529  reuan  27829  afvfv0bi  27887  ffnafv  27906  fzo1fzo0n0  27992  usg2spthonot1  28091  frgra0v  28101  com3rgbi  28312  pm2.43bgbi  28315  pm2.43cbi  28316  sb5ALT  28324  trsbc  28340  2pm13.193  28354  a9e2ndeq  28361  2uasbanh  28363  eelT01  28531  eel0T1  28532  uunT1  28605  zfregs2VD  28666  equncomVD  28693  trsbcVD  28702  undif3VD  28707  2pm13.193VD  28728  a9e2eqVD  28732  a9e2ndeqVD  28734  2uasbanhVD  28736  a9e2ndeqALT  28757  bnj1533  28933  bnj983  29032  alcomwAUX7  29154  ax12olem3aAUX7  29167  equsalNEW7  29197  cbvalwwAUX7  29227  equvinNEW7  29237  sbnNEW7  29270  sbimNEW7  29273  sb5rfNEW7  29296  sb6rfNEW7  29297  sb8wAUX7  29298  equs45fNEW7  29326  sb6fNEW7  29338  dfsb2NEW7  29343  alcomw9bAUX7  29365  alcomOLD7  29369  excomOLD7  29382  cbvalOLD7  29413  nfsb4tw2AUXOLD7  29434  sbcomOLD7  29443  sb8OLD7  29444  sb9iOLD7  29446  sb9OLD7  29447  isltrn2N  30606
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