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

Theorem impbii 180
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 179 . 2  |-  ( (
ph  ->  ps )  -> 
( ( ps  ->  ph )  ->  ( ph  <->  ps ) ) )
41, 2, 3mp2 17 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  dfbi1  184  bicom  191  biid  227  2th  230  pm5.74  235  bitri  240  notnot  282  con34b  283  notbi  286  bibi2i  304  con1b  323  con2b  324  bi2.04  350  pm5.4  351  imdi  352  pm4.8  354  pm4.81  355  orcom  376  dfor2  400  impexp  433  ancom  437  oridm  500  orbi2i  505  or12  509  pm4.45im  545  pm4.44  560  pm4.79  566  anass  630  jaob  758  jcab  833  andi  837  pm4.72  846  oibabs  851  pm4.82  894  consensus  925  rnlem  931  3jaob  1244  truan  1331  dfnot  1332  3impexp  1366  3impexpbicom  1367  cad1  1398  tbw-bijust  1463  tbw-negdf  1464  19.26  1593  sbbii  1653  19.9v  1664  equcom  1680  ax12b  1689  19.3vOLD  1696  cbvalw  1701  cbvalvw  1702  alcom  1737  19.9hOLD  1782  19.3  1786  19.23hOLD  1822  equsalhwOLD  1844  19.21hOLD  1845  excomOLD  1864  19.41  1882  19.41OLD  1883  ax12olem1  1932  ax12olem3  1934  equsal  1965  cbval  1989  equs45f  1994  equvin  2006  sb6f  2044  dfsb2  2060  sbn  2067  sbim  2070  sb5rf  2095  sb6rf  2096  sb9  2100  mo  2231  eu2  2234  mo2  2238  exmoeu  2251  euan  2266  2mo  2287  2eu6  2294  axext4  2342  cleqh  2455  nebi  2592  r19.26  2751  ralcom3  2781  ceqsex  2898  gencbvex  2906  gencbvex2  2907  eqvinc  2971  pm13.183  2984  rr19.3v  2985  rr19.28v  2986  euxfr2  3026  reu6  3030  reu3  3031  sbnfc2  3217  sspss  3351  unineq  3495  uneqin  3496  undif3  3505  difrab  3518  un00  3566  ssdifeq0  3612  r19.2zb  3620  ralf0  3636  elpr2  3735  snidb  3742  difsnb  3836  pwpw0  3842  sssn  3853  preq12b  3869  preqsn  3873  pwsnALT  3903  unissint  3967  uniintsn  3980  iununi  4067  intex  4248  intnex  4249  iin0  4265  axpweq  4268  nfcvb  4286  sspwb  4305  unipw  4306  opnz  4324  opth  4327  opthwiener  4350  ssopab2b  4373  pwssun  4381  pwundifOLD  4382  elon2  4485  unexb  4602  eusvnfb  4612  eusv2nf  4614  ralxfrALT  4635  uniexb  4645  iunpw  4652  ordeleqon  4662  onintrab  4674  unon  4704  onuninsuci  4713  ordzsl  4718  onzsl  4719  opelxp  4801  opthprc  4818  relop  4916  issetid  4920  xpid11  4982  elres  5072  iss  5080  issref  5138  asymref2  5142  xpnz  5181  ssrnres  5198  dfrel2  5206  relrelss  5278  unixp0  5288  fn0  5445  funssxp  5485  f00  5509  dffo2  5538  ffoss  5588  f1o00  5591  fo00  5592  fv3  5624  dffn5  5651  dff2  5755  dff3  5756  dffo4  5759  dffo5  5760  exfo  5761  fmpt  5764  ffnfv  5768  fsn  5779  fsn2  5781  fconstfv  5820  isores1  5918  ssoprab2b  5992  eqfnov2  6038  1st2ndb  6247  reldmtpos  6329  riotaundb  6433  abianfp  6558  omopthi  6742  mapsn  6897  mapsncnv  6902  mptelixpg  6941  elixpsn  6943  ixpsnf1o  6944  bren2  6980  en0  7012  en1  7016  en1b  7017  sbthb  7070  canth2  7102  onfin2  7140  sdom1  7150  1sdom  7153  fineqv  7166  unfilem1  7211  fiint  7223  pwfi  7241  unifpw  7248  wofib  7350  sucprcreg  7403  opthreg  7409  suc11reg  7410  infeq5  7428  rankwflemb  7555  r1elss  7568  pwwf  7569  unwf  7572  uniwf  7581  rankonid  7591  rankr1id  7624  rankuni  7625  rankxplim3  7641  scott0  7646  karden  7655  isnum3  7677  oncard  7683  card1  7691  cardlim  7695  cardmin2  7721  pm54.43lem  7722  ween  7752  acnnum  7769  alephsuc2  7797  alephgeom  7799  iscard3  7810  dfac3  7838  dfac4  7839  dfac5lem3  7842  dfac5  7845  dfac2  7847  dfac8  7851  dfac9  7852  dfacacn  7857  dfac13  7858  dfac12r  7862  dfac12k  7863  kmlem2  7867  kmlem13  7878  cdainf  7908  ackbij2  7959  cflim2  7979  isfin4-2  8030  isfin4-3  8031  isf33lem  8082  compsscnv  8087  fin1a2lem6  8121  domtriom  8159  ac9  8200  ac9s  8210  fodomb  8241  brdom3  8243  brdom5  8244  brdom4  8245  brdom7disj  8246  brdom6disj  8247  iunfo  8251  sdomsdomcard  8272  gch2  8391  gch3  8392  eltsk2g  8463  grutsk  8534  grothpw  8538  ordpipq  8656  ltbtwnnq  8692  mappsrpr  8820  map2psrpr  8822  elreal2  8844  le2tri3i  9039  ltadd2i  9040  elnn0nn  10098  elnnnn0b  10100  elnnnn0c  10101  elnnz  10126  elnn0z  10128  elz2  10132  elnnz1  10141  eluz2b2  10382  elnn1uz2  10386  elioo4g  10803  eluzfz2b  10897  fzn0  10901  elfz1end  10912  fzass4  10921  fzolb  10972  fzon0  10983  elfzo0  10996  om2uzrani  11107  nn0opthi  11378  hashkf  11432  hashf1  11491  wrdexb  11545  sqr0lem  11822  rexanuz  11925  rexuz3  11928  fsum0diag  12337  sadcp1  12743  isprm6  12885  4sqlem4  13096  mreunirn  13602  isdrs2  14172  isacs5  14374  isacs4  14375  isacs3  14376  isnsg3  14750  gicer  14839  oppgmndb  14927  oppggrpb  14930  invghm  15229  opprrngb  15513  abvn0b  16142  gzrngunit  16543  zrngunit  16544  dvdsrz  16546  zlmlmod  16583  zlmassa  16584  cygth  16631  frgpcyg  16633  tgclb  16814  iscldtop  16938  isnrm2  17192  isnrm3  17193  discmp  17231  dfcon2  17251  2ndcsb  17281  dis2ndc  17292  loclly  17319  iskgen2  17349  dfac14  17418  kqtop  17542  kqt0  17543  kqreg  17548  kqnrm  17549  hmpher  17581  hmphsymb  17583  hmph0  17592  kqhmph  17616  ist1-5lem  17617  elmptrab2  17625  isfil2  17653  filunirn  17679  isufil2  17705  hausflim  17778  isfcls  17806  alexsubALT  17847  istgp2  17876  xmetunirn  18004  dscmet  18197  dscopn  18198  isngp4  18235  zcld  18421  zlmclm  18697  iscmet2  18824  iundisj  19009  i1f1lem  19148  fta1b  19659  elply2  19682  elqaa  19806  aannenlem2  19813  wilth  20421  lgsne0  20684  2sqlem2  20715  ostth  20900  nmlno0lem  21485  isblo3i  21493  blocni  21497  hvsubeq0i  21756  hvaddcani  21758  bcseqi  21813  isch3  21935  norm1exi  21943  hhsssh  21960  shslubi  22078  dfch2  22100  pjoc1i  22124  pjchi  22125  shs00i  22143  chsscon3i  22154  chlejb1i  22169  chj00i  22180  shjshseli  22186  h1de2ctlem  22248  spanunsni  22272  cmcmi  22285  cmbr3i  22293  cmbr4i  22294  pj11i  22404  hosubeq0i  22520  dmadjrnb  22600  nmlnop0iALT  22689  lnopeq0i  22701  elunop2  22707  lnconi  22727  lncnopbd  22731  adjbdlnb  22778  adjbd1o  22779  adjeq0  22785  rnbra  22801  pjss1coi  22857  pjss2coi  22858  pjnormssi  22862  pjssdif2i  22868  pjssdif1i  22869  dfpjop  22876  pjinvari  22885  pjin2i  22887  pjci  22894  pjcmul1i  22895  pjcmul2i  22896  strb  22952  hstrbi  22960  mdsl1i  23015  atom1d  23047  chrelat2i  23059  cvbr4i  23061  cvexchi  23063  sumdmdi  23114  dmdbr4ati  23115  dmdbr5ati  23116  dmdbr6ati  23117  dmdbr7ati  23118  cdj3i  23135  bisimp  23142  difeq  23196  iundisjf  23227  feqmptdf  23279  elfzo1  23355  iundisjfi  23356  xrge0tsmsbi  23416  ustbas  23531  issgon  23772  measbasedom  23821  ballotlem2  23995  ballotlemrinv  24040  wrdumgra  24272  nepss  24476  dfpo2  24670  dfon2  24706  distel  24718  elno2  24866  bdayfo  24887  elfix  25001  dffix2  25003  fnimage  25026  altopthsn  25054  mptelee  25082  ellines  25334  rankeq1o  25360  df3nandALT1  25394  wl-pm5.74lem  25476  volsupnfl  25491  opnrebl2  25560  locfindis  25629  cover2  25682  isbnd3  25831  cntotbnd  25843  heibor  25868  isfld2  25953  isfldidl  26016  prtlem16  26060  funsnfsup  26085  ismrc  26099  isnacs3  26108  rexzrexnn0  26208  eldioph4b  26217  dford3  26444  wopprc  26446  ttac  26452  pw2f1ocnv  26453  dfac11  26483  dfac21  26487  isnumbasabl  26594  isnumbasgrp  26595  dfacbasgrp  26596  aaitgo  26690  pmtrfb  26729  pm10.55  26887  pm11.57  26911  sbeqalbi  26923  pm13.192  26933  pm13.194  26935  ipo0  26975  ifr0  26976  xpexb  26981  reuan  27281  afvfv0bi  27340  ffnafv  27359  tppreqb  27408  hashprb  27470  uhgra0v  27517  usgra0v  27546  uvtx01vtx  27655  istrl2  27690  frgra0v  27826  com3rgbi  28021  pm2.43bgbi  28024  pm2.43cbi  28025  sb5ALT  28033  trsbc  28049  2pm13.193  28063  a9e2ndeq  28070  2uasbanh  28072  eelT01  28241  eel0T1  28242  uunT1  28315  zfregs2VD  28379  equncomVD  28406  trsbcVD  28415  undif3VD  28420  2pm13.193VD  28441  a9e2eqVD  28445  a9e2ndeqVD  28447  2uasbanhVD  28449  a9e2ndeqALT  28470  bnj1533  28646  bnj983  28745  alcomwAUX7  28867  ax12olem3aAUX7  28880  equsalNEW7  28910  cbvalwwAUX7  28940  equvinNEW7  28950  sbnNEW7  28983  sbimNEW7  28986  sb5rfNEW7  29009  sb6rfNEW7  29010  sb8wAUX7  29011  equs45fNEW7  29039  sb6fNEW7  29051  dfsb2NEW7  29056  alcomw9bAUX7  29078  alcomOLD7  29082  excomOLD7  29095  cbvalOLD7  29126  nfsb4tw2AUXOLD7  29147  sbcomOLD7  29156  sb8OLD7  29157  sb9iOLD7  29159  sb9OLD7  29160  equvinv  29183  equvelv  29185  isltrn2N  30378
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 177
  Copyright terms: Public domain W3C validator