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  1582  sbbii  1636  equcom  1649  ax12b  1657  19.3v  1664  cbvalw  1677  cbvalvw  1678  alcom  1713  19.9h  1729  19.23h  1730  equsalhw  1732  19.21h  1733  19.3  1783  excom  1788  19.41  1817  ax12olem1  1870  ax12olem3  1872  equsal  1902  cbval  1926  equs45f  1931  equvin  1943  sb6f  1981  dfsb2  1997  sbn  2004  sbim  2007  sb5rf  2032  sb6rf  2033  sb8  2034  sb9  2037  mo  2167  eu2  2170  mo2  2174  exmoeu  2187  euan  2202  2mo  2223  2eu6  2230  axext4  2269  cleqh  2382  nebi  2519  r19.26  2677  ralcom3  2707  ceqsex  2824  gencbvex  2832  gencbvex2  2833  eqvinc  2897  pm13.183  2910  rr19.3v  2911  rr19.28v  2912  euxfr2  2952  reu6  2956  reu3  2957  sbnfc2  3143  sspss  3277  unineq  3421  uneqin  3422  undif3  3431  difrab  3444  un00  3492  ssdifeq0  3538  r19.2zb  3546  ralf0  3562  elpr2  3661  snidb  3668  difsneq  3759  pwpw0  3765  sssn  3774  preq12b  3790  preqsn  3794  pwsnALT  3824  unissint  3888  uniintsn  3901  iununi  3988  intex  4169  intnex  4170  iin0  4186  axpweq  4189  nfcvb  4207  sspwb  4225  unipw  4226  opnz  4244  opth  4247  opthwiener  4270  ssopab2b  4293  pwssun  4301  pwundifOLD  4303  elon2  4405  unexb  4522  eusvnfb  4532  eusv2nf  4534  ralxfrALT  4555  uniexb  4565  iunpw  4572  ordeleqon  4582  onintrab  4594  unon  4624  onuninsuci  4633  ordzsl  4638  onzsl  4639  opelxp  4721  opthprc  4738  relop  4836  issetid  4840  xpid11  4902  elres  4992  iss  5000  issref  5058  asymref2  5062  xpnz  5101  ssrnres  5118  dfrel2  5126  relrelss  5198  unixp0  5208  fn0  5365  funssxp  5404  f00  5428  dffo2  5457  ffoss  5507  f1o00  5510  fo00  5511  fv3  5543  dffn5  5570  dff2  5674  dff3  5675  dffo4  5678  dffo5  5679  exfo  5680  fmpt  5683  ffnfv  5687  fsn  5698  fsn2  5700  fconstfv  5736  isores1  5833  ssoprab2b  5907  eqfnov2  5953  1st2ndb  6162  reldmtpos  6244  riotaundb  6348  abianfp  6473  omopthi  6657  mapsn  6811  mapsncnv  6816  mptelixpg  6855  elixpsn  6857  ixpsnf1o  6858  bren2  6894  en0  6926  en1  6930  en1b  6931  sbthb  6984  canth2  7016  onfin2  7054  sdom1  7064  1sdom  7067  fineqv  7080  unfilem1  7123  fiint  7135  pwfi  7153  unifpw  7160  wofib  7262  sucprcreg  7315  opthreg  7321  suc11reg  7322  infeq5  7340  rankwflemb  7467  r1elss  7480  pwwf  7481  unwf  7484  uniwf  7493  rankonid  7503  rankr1id  7536  rankuni  7537  rankxplim3  7553  scott0  7558  karden  7567  isnum3  7589  oncard  7595  card1  7603  cardlim  7607  cardmin2  7633  pm54.43lem  7634  ween  7664  acnnum  7681  alephsuc2  7709  alephgeom  7711  iscard3  7722  dfac3  7750  dfac4  7751  dfac5lem3  7754  dfac5  7757  dfac2  7759  dfac8  7763  dfac9  7764  dfacacn  7769  dfac13  7770  dfac12r  7774  dfac12k  7775  kmlem2  7779  kmlem13  7790  cdainf  7820  ackbij2  7871  cflim2  7891  isfin4-2  7942  isfin4-3  7943  isf33lem  7994  compsscnv  7999  fin1a2lem6  8033  domtriom  8071  ac9  8112  ac9s  8122  fodomb  8153  brdom3  8155  brdom5  8156  brdom4  8157  brdom7disj  8158  brdom6disj  8159  iunfo  8163  sdomsdomcard  8184  gch2  8303  gch3  8304  eltsk2g  8375  grutsk  8446  grothpw  8450  ordpipq  8568  ltbtwnnq  8604  mappsrpr  8732  map2psrpr  8734  elreal2  8756  le2tri3i  8951  ltadd2i  8952  elnn0nn  10008  elnnnn0b  10010  elnnnn0c  10011  elnnz  10036  elnn0z  10038  elz2  10042  elnnz1  10051  eluz2b2  10292  elnn1uz2  10296  elioo4g  10713  eluzfz2b  10807  fzn0  10811  elfz1end  10822  fzass4  10831  fzolb  10882  fzon0  10893  elfzo0  10906  om2uzrani  11017  nn0opthi  11287  hashkf  11341  hashf1  11397  wrdexb  11451  sqr0lem  11728  rexanuz  11831  rexuz3  11834  fsum0diag  12242  sadcp1  12648  isprm6  12790  4sqlem4  13001  mreunirn  13505  isdrs2  14075  isacs5  14277  isacs4  14278  isacs3  14279  isnsg3  14653  gicer  14742  oppgmndb  14830  oppggrpb  14833  invghm  15132  opprrngb  15416  abvn0b  16045  gzrngunit  16439  zrngunit  16440  dvdsrz  16442  zlmlmod  16479  zlmassa  16480  cygth  16527  frgpcyg  16529  tgclb  16710  iscldtop  16834  isnrm2  17088  isnrm3  17089  discmp  17127  dfcon2  17147  2ndcsb  17177  dis2ndc  17188  loclly  17215  iskgen2  17245  dfac14  17314  kqtop  17438  kqt0  17439  kqreg  17444  kqnrm  17445  hmpher  17477  hmphsymb  17479  hmph0  17488  kqhmph  17512  ist1-5lem  17513  elmptrab2  17525  isfil2  17553  filunirn  17579  isufil2  17605  hausflim  17678  isfcls  17706  alexsubALT  17747  istgp2  17776  xmetunirn  17904  dscmet  18097  dscopn  18098  isngp4  18135  zcld  18321  zlmclm  18595  iscmet2  18722  iundisj  18907  i1f1lem  19046  fta1b  19557  elply2  19580  elqaa  19704  aannenlem2  19711  wilth  20311  lgsne0  20574  2sqlem2  20605  ostth  20790  nmlno0lem  21373  isblo3i  21381  blocni  21385  hvsubeq0i  21644  hvaddcani  21646  bcseqi  21701  isch3  21823  norm1exi  21831  hhsssh  21848  shslubi  21966  dfch2  21988  pjoc1i  22012  pjchi  22013  shs00i  22031  chsscon3i  22042  chlejb1i  22057  chj00i  22068  shjshseli  22074  h1de2ctlem  22136  spanunsni  22160  cmcmi  22173  cmbr3i  22181  cmbr4i  22182  pj11i  22292  hosubeq0i  22408  dmadjrnb  22488  nmlnop0iALT  22577  lnopeq0i  22589  elunop2  22595  lnconi  22615  lncnopbd  22619  adjbdlnb  22666  adjbd1o  22667  adjeq0  22673  rnbra  22689  pjss1coi  22745  pjss2coi  22746  pjnormssi  22750  pjssdif2i  22756  pjssdif1i  22757  dfpjop  22764  pjinvari  22773  pjin2i  22775  pjci  22782  pjcmul1i  22783  pjcmul2i  22784  strb  22840  hstrbi  22848  mdsl1i  22903  atom1d  22935  chrelat2i  22947  cvbr4i  22949  cvexchi  22951  sumdmdi  23002  dmdbr4ati  23003  dmdbr5ati  23004  dmdbr6ati  23005  dmdbr7ati  23006  cdj3i  23023  ballotlem2  23049  ballotlemrinv  23094  bisimp  23123  difeq  23130  feqmptdf  23230  elfzo1  23281  iundisjfi  23365  iundisjf  23367  xrge0tsmsbi  23385  issgon  23486  measbasedom  23534  wrdumgra  23870  nepss  24074  dfpo2  24114  dfon2  24150  distel  24162  elno2  24310  bdayfo  24331  elfix  24445  dffix2  24447  fnimage  24470  altopthsn  24497  mptelee  24525  ellines  24777  rankeq1o  24803  df3nandALT1  24837  wl-pm5.74lem  24919  and4as  24950  altdftru  24959  trcrm  24962  facrm  24964  bibox  24993  binxt  24995  nxtor  24996  nxtand  24997  bidia  25000  evpexun  25009  alalifal  25014  boxand  25017  axlll2  25039  dmoprabss6  25046  restidsing  25087  fixpc  25105  sssu  25152  dstr  25182  definc  25290  domncnt  25293  ranncnt  25294  dfps2  25300  sallnei  25540  altretop  25611  addcanri  25677  bisig0  26073  opnrebl2  26247  locfindis  26316  cover2  26369  isbnd3  26519  cntotbnd  26531  heibor  26556  isfld2  26641  isfldidl  26704  prtlem16  26748  funsnfsup  26773  ismrc  26787  isnacs3  26796  rexzrexnn0  26896  eldioph4b  26905  dford3  27132  wopprc  27134  ttac  27140  pw2f1ocnv  27141  dfac11  27171  dfac21  27175  isnumbasabl  27282  isnumbasgrp  27283  dfacbasgrp  27284  aaitgo  27378  pmtrfb  27417  pm10.55  27575  pm11.57  27599  sbeqalbi  27611  pm13.192  27621  pm13.194  27623  ipo0  27663  ifr0  27664  xpexb  27669  reuan  27969  afvfv0bi  28026  ffnafv  28044  usgra0v  28128  uvtx01vtx  28175  frgra0v  28185  com3rgbi  28332  pm2.43bgbi  28335  pm2.43cbi  28336  sb5ALT  28344  trsbc  28360  2pm13.193  28374  a9e2ndeq  28381  2uasbanh  28383  eelT01  28552  eel0T1  28553  uunT1  28626  zfregs2VD  28690  equncomVD  28717  trsbcVD  28726  undif3VD  28731  2pm13.193VD  28752  a9e2eqVD  28756  a9e2ndeqVD  28758  2uasbanhVD  28760  a9e2ndeqALT  28781  bnj1533  28957  bnj983  29056  equvinv  29187  equvelv  29189  isltrn2N  30382
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