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  dfnot  1322  3impexp  1356  3impexpbicom  1357  cad1  1388  tbw-bijust  1453  tbw-negdf  1454  19.26  1580  sbbii  1634  equcom  1647  ax12b  1655  19.3v  1662  cbvalw  1675  cbvalvw  1676  alcom  1711  19.9h  1727  19.23h  1728  equsalhw  1730  19.21h  1731  19.3  1781  excom  1786  19.41  1815  ax12olem1  1868  ax12olem3  1870  equsal  1900  cbval  1924  equs45f  1929  equvin  1941  sb6f  1979  dfsb2  1995  sbn  2002  sbim  2005  sb5rf  2030  sb6rf  2031  sb8  2032  sb9  2035  mo  2165  eu2  2168  mo2  2172  exmoeu  2185  euan  2200  2mo  2221  2eu6  2228  axext4  2267  cleqh  2380  nebi  2517  r19.26  2675  ralcom3  2705  ceqsex  2822  gencbvex  2830  gencbvex2  2831  eqvinc  2895  pm13.183  2908  rr19.3v  2909  rr19.28v  2910  euxfr2  2950  reu6  2954  reu3  2955  sbnfc2  3141  sspss  3275  unineq  3419  uneqin  3420  undif3  3429  difrab  3442  un00  3490  ssdifeq0  3536  r19.2zb  3544  ralf0  3560  elpr2  3659  snidb  3666  difsneq  3757  pwpw0  3763  sssn  3772  preq12b  3788  preqsn  3792  pwsnALT  3822  unissint  3886  uniintsn  3899  iununi  3986  intex  4167  intnex  4168  iin0  4184  axpweq  4187  nfcvb  4205  sspwb  4223  unipw  4224  opnz  4242  opth  4245  opthwiener  4268  ssopab2b  4291  pwssun  4299  pwundifOLD  4301  elon2  4403  unexb  4520  eusvnfb  4530  eusv2nf  4532  ralxfrALT  4553  uniexb  4563  iunpw  4570  ordeleqon  4580  onintrab  4592  unon  4622  onuninsuci  4631  ordzsl  4636  onzsl  4637  opelxp  4719  opthprc  4736  relop  4834  issetid  4838  xpid11  4900  elres  4990  iss  4998  issref  5056  asymref2  5060  xpnz  5099  ssrnres  5116  dfrel2  5124  relrelss  5196  unixp0  5206  fn0  5363  funssxp  5402  f00  5426  dffo2  5455  ffoss  5505  f1o00  5508  fo00  5509  fv3  5541  dffn5  5568  dff2  5672  dff3  5673  dffo4  5676  dffo5  5677  exfo  5678  fmpt  5681  ffnfv  5685  fsn  5696  fsn2  5698  fconstfv  5734  isores1  5831  ssoprab2b  5905  eqfnov2  5951  1st2ndb  6160  reldmtpos  6242  riotaundb  6346  abianfp  6471  omopthi  6655  mapsn  6809  mapsncnv  6814  mptelixpg  6853  elixpsn  6855  ixpsnf1o  6856  bren2  6892  en0  6924  en1  6928  en1b  6929  sbthb  6982  canth2  7014  onfin2  7052  sdom1  7062  1sdom  7065  fineqv  7078  unfilem1  7121  fiint  7133  pwfi  7151  unifpw  7158  wofib  7260  sucprcreg  7313  opthreg  7319  suc11reg  7320  infeq5  7338  rankwflemb  7465  r1elss  7478  pwwf  7479  unwf  7482  uniwf  7491  rankonid  7501  rankr1id  7534  rankuni  7535  rankxplim3  7551  scott0  7556  karden  7565  isnum3  7587  oncard  7593  card1  7601  cardlim  7605  cardmin2  7631  pm54.43lem  7632  ween  7662  acnnum  7679  alephsuc2  7707  alephgeom  7709  iscard3  7720  dfac3  7748  dfac4  7749  dfac5lem3  7752  dfac5  7755  dfac2  7757  dfac8  7761  dfac9  7762  dfacacn  7767  dfac13  7768  dfac12r  7772  dfac12k  7773  kmlem2  7777  kmlem13  7788  cdainf  7818  ackbij2  7869  cflim2  7889  isfin4-2  7940  isfin4-3  7941  isf33lem  7992  compsscnv  7997  fin1a2lem6  8031  domtriom  8069  ac9  8110  ac9s  8120  fodomb  8151  brdom3  8153  brdom5  8154  brdom4  8155  brdom7disj  8156  brdom6disj  8157  iunfo  8161  sdomsdomcard  8182  gch2  8301  gch3  8302  eltsk2g  8373  grutsk  8444  grothpw  8448  ordpipq  8566  ltbtwnnq  8602  mappsrpr  8730  map2psrpr  8732  elreal2  8754  le2tri3i  8949  ltadd2i  8950  elnn0nn  10006  elnnnn0b  10008  elnnnn0c  10009  elnnz  10034  elnn0z  10036  elz2  10040  elnnz1  10049  eluz2b2  10290  elnn1uz2  10294  elioo4g  10711  eluzfz2b  10805  fzn0  10809  elfz1end  10820  fzass4  10829  fzolb  10880  fzon0  10891  elfzo0  10904  om2uzrani  11015  nn0opthi  11285  hashkf  11339  hashf1  11395  wrdexb  11449  sqr0lem  11726  rexanuz  11829  rexuz3  11832  fsum0diag  12240  sadcp1  12646  isprm6  12788  4sqlem4  12999  mreunirn  13503  isdrs2  14073  isacs5  14275  isacs4  14276  isacs3  14277  isnsg3  14651  gicer  14740  oppgmndb  14828  oppggrpb  14831  invghm  15130  opprrngb  15414  abvn0b  16043  gzrngunit  16437  zrngunit  16438  dvdsrz  16440  zlmlmod  16477  zlmassa  16478  cygth  16525  frgpcyg  16527  tgclb  16708  iscldtop  16832  isnrm2  17086  isnrm3  17087  discmp  17125  dfcon2  17145  2ndcsb  17175  dis2ndc  17186  loclly  17213  iskgen2  17243  dfac14  17312  kqtop  17436  kqt0  17437  kqreg  17442  kqnrm  17443  hmpher  17475  hmphsymb  17477  hmph0  17486  kqhmph  17510  ist1-5lem  17511  elmptrab2  17523  isfil2  17551  filunirn  17577  isufil2  17603  hausflim  17676  isfcls  17704  alexsubALT  17745  istgp2  17774  xmetunirn  17902  dscmet  18095  dscopn  18096  isngp4  18133  zcld  18319  zlmclm  18593  iscmet2  18720  iundisj  18905  i1f1lem  19044  fta1b  19555  elply2  19578  elqaa  19702  aannenlem2  19709  wilth  20309  lgsne0  20572  2sqlem2  20603  ostth  20788  nmlno0lem  21371  isblo3i  21379  blocni  21383  hvsubeq0i  21642  hvaddcani  21644  bcseqi  21699  isch3  21821  norm1exi  21829  hhsssh  21846  shslubi  21964  dfch2  21986  pjoc1i  22010  pjchi  22011  shs00i  22029  chsscon3i  22040  chlejb1i  22055  chj00i  22066  shjshseli  22072  h1de2ctlem  22134  spanunsni  22158  cmcmi  22171  cmbr3i  22179  cmbr4i  22180  pj11i  22290  hosubeq0i  22406  dmadjrnb  22486  nmlnop0iALT  22575  lnopeq0i  22587  elunop2  22593  lnconi  22613  lncnopbd  22617  adjbdlnb  22664  adjbd1o  22665  adjeq0  22671  rnbra  22687  pjss1coi  22743  pjss2coi  22744  pjnormssi  22748  pjssdif2i  22754  pjssdif1i  22755  dfpjop  22762  pjinvari  22771  pjin2i  22773  pjci  22780  pjcmul1i  22781  pjcmul2i  22782  strb  22838  hstrbi  22846  mdsl1i  22901  atom1d  22933  chrelat2i  22945  cvbr4i  22947  cvexchi  22949  sumdmdi  23000  dmdbr4ati  23001  dmdbr5ati  23002  dmdbr6ati  23003  dmdbr7ati  23004  cdj3i  23021  ballotlem2  23047  ballotlemrinv  23092  bisimp  23121  difeq  23128  feqmptdf  23228  elfzo1  23279  iundisjfi  23363  iundisjf  23365  xrge0tsmsbi  23383  issgon  23484  measbasedom  23532  wrdumgra  23868  nepss  24072  dfpo2  24112  dfon2  24148  distel  24160  elno2  24308  bdayfo  24329  elfix  24443  dffix2  24445  fnimage  24468  altopthsn  24495  mptelee  24523  ellines  24775  rankeq1o  24801  df3nandALT1  24835  wl-pm5.74lem  24917  and4as  24939  altdftru  24948  trcrm  24951  facrm  24953  bibox  24982  binxt  24984  nxtor  24985  nxtand  24986  bidia  24989  evpexun  24998  alalifal  25003  boxand  25006  axlll2  25028  dmoprabss6  25035  restidsing  25076  fixpc  25094  sssu  25141  dstr  25171  definc  25279  domncnt  25282  ranncnt  25283  dfps2  25289  sallnei  25529  altretop  25600  addcanri  25666  bisig0  26062  opnrebl2  26236  locfindis  26305  cover2  26358  isbnd3  26508  cntotbnd  26520  heibor  26545  isfld2  26630  isfldidl  26693  prtlem16  26737  funsnfsup  26762  ismrc  26776  isnacs3  26785  rexzrexnn0  26885  eldioph4b  26894  dford3  27121  wopprc  27123  ttac  27129  pw2f1ocnv  27130  dfac11  27160  dfac21  27164  isnumbasabl  27271  isnumbasgrp  27272  dfacbasgrp  27273  aaitgo  27367  pmtrfb  27406  pm10.55  27564  pm11.57  27588  sbeqalbi  27600  pm13.192  27610  pm13.194  27612  ipo0  27652  ifr0  27653  xpexb  27658  reuan  27958  afvfv0bi  28015  ffnafv  28033  usgra0v  28117  uvtx01vtx  28164  frgra0v  28174  com3rgbi  28276  pm2.43bgbi  28279  pm2.43cbi  28280  sb5ALT  28288  trsbc  28304  2pm13.193  28318  a9e2ndeq  28325  2uasbanh  28327  eelT01  28489  eel0T1  28490  uunT1  28555  zfregs2VD  28617  equncomVD  28644  trsbcVD  28653  undif3VD  28658  2pm13.193VD  28679  a9e2eqVD  28683  a9e2ndeqVD  28685  2uasbanhVD  28687  a9e2ndeqALT  28708  bnj1533  28884  bnj983  28983  equvinv  29114  equvelv  29116  isltrn2N  30309
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