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  1635  equcom  1648  ax12b  1656  19.3v  1663  cbvalw  1676  cbvalvw  1677  alcom  1712  19.9h  1729  19.23h  1730  equsalhw  1732  19.21h  1733  19.3  1783  excom  1788  19.41  1817  ax12olem1  1870  ax12olem3  1872  equsal  1903  cbval  1927  equs45f  1932  equvin  1946  sb6f  1984  dfsb2  1994  sbn  2001  sbim  2004  sb5rf  2029  sb6rf  2030  sb8  2031  sb9  2034  mo  2166  eu2  2169  mo2  2173  exmoeu  2186  euan  2201  2mo  2222  2eu6  2229  axext4  2268  cleqh  2381  nebi  2518  r19.26  2676  ralcom3  2706  ceqsex  2823  gencbvex  2831  gencbvex2  2832  eqvinc  2896  pm13.183  2909  rr19.3v  2910  rr19.28v  2911  euxfr2  2951  reu6  2955  reu3  2956  sbnfc2  3142  sspss  3276  unineq  3420  uneqin  3421  undif3  3430  difrab  3443  un00  3491  ssdifeq0  3537  r19.2zb  3545  ralf0  3561  elpr2  3660  snidb  3667  difsneq  3758  pwpw0  3764  sssn  3773  preq12b  3789  preqsn  3793  pwsnALT  3823  unissint  3887  uniintsn  3900  iununi  3987  intex  4170  intnex  4171  iin0  4183  axpweq  4186  nfcvb  4204  sspwb  4222  unipw  4223  opnz  4241  opth  4244  opthwiener  4267  ssopab2b  4290  pwssun  4298  pwundifOLD  4300  elon2  4402  unexb  4519  eusvnfb  4529  eusv2nf  4531  ralxfrALT  4552  uniexb  4562  iunpw  4569  ordeleqon  4579  onintrab  4591  unon  4621  onuninsuci  4630  ordzsl  4635  onzsl  4636  opelxp  4718  opthprc  4735  relop  4833  issetid  4837  xpid11  4899  elres  4989  iss  4997  issref  5055  asymref2  5059  xpnz  5098  ssrnres  5115  dfrel2  5123  relrelss  5194  unixp0  5204  fn0  5329  funssxp  5368  f00  5392  dffo2  5421  ffoss  5471  f1o00  5474  fo00  5475  fv3  5502  dffn5  5530  dff2  5634  dff3  5635  dffo4  5638  dffo5  5639  exfo  5640  fmpt  5643  ffnfv  5647  fsn  5658  fsn2  5660  fconstfv  5696  isores1  5793  ssoprab2b  5867  eqfnov2  5913  1st2ndb  6122  reldmtpos  6204  riotaundb  6342  abianfp  6467  omopthi  6651  mapsn  6805  mapsncnv  6810  mptelixpg  6849  elixpsn  6851  ixpsnf1o  6852  bren2  6888  en0  6920  en1  6924  en1b  6925  sbthb  6978  canth2  7010  onfin2  7048  sdom1  7058  1sdom  7061  fineqv  7074  unfilem1  7117  fiint  7129  pwfi  7147  unifpw  7154  wofib  7256  sucprcreg  7309  opthreg  7315  suc11reg  7316  infeq5  7334  rankwflemb  7461  r1elss  7474  pwwf  7475  unwf  7478  uniwf  7487  rankonid  7497  rankr1id  7530  rankuni  7531  rankxplim3  7547  scott0  7552  karden  7561  isnum3  7583  oncard  7589  card1  7597  cardlim  7601  cardmin2  7627  pm54.43lem  7628  ween  7658  acnnum  7675  alephsuc2  7703  alephgeom  7705  iscard3  7716  dfac3  7744  dfac4  7745  dfac5lem3  7748  dfac5  7751  dfac2  7753  dfac8  7757  dfac9  7758  dfacacn  7763  dfac13  7764  dfac12r  7768  dfac12k  7769  kmlem2  7773  kmlem13  7784  cdainf  7814  ackbij2  7865  cflim2  7885  isfin4-2  7936  isfin4-3  7937  isf33lem  7988  compsscnv  7993  fin1a2lem6  8027  domtriom  8065  ac9  8106  ac9s  8116  fodomb  8147  brdom3  8149  brdom5  8150  brdom4  8151  brdom7disj  8152  brdom6disj  8153  iunfo  8157  sdomsdomcard  8178  gch2  8297  gch3  8298  eltsk2g  8369  grutsk  8440  grothpw  8444  ordpipq  8562  ltbtwnnq  8598  mappsrpr  8726  map2psrpr  8728  elreal2  8750  le2tri3i  8945  ltadd2i  8946  elnn0nn  10002  elnnnn0b  10004  elnnnn0c  10005  elnnz  10030  elnn0z  10032  elz2  10036  elnnz1  10045  eluz2b2  10286  elnn1uz2  10290  elioo4g  10707  eluzfz2b  10801  fzn0  10805  elfz1end  10816  fzass4  10825  fzolb  10876  fzon0  10887  elfzo0  10900  om2uzrani  11011  nn0opthi  11281  hashkf  11335  hashf1  11391  wrdexb  11445  sqr0lem  11722  rexanuz  11825  rexuz3  11828  fsum0diag  12236  sadcp1  12642  isprm6  12784  4sqlem4  12995  mreunirn  13499  isdrs2  14069  isacs5  14271  isacs4  14272  isacs3  14273  isnsg3  14647  gicer  14736  oppgmndb  14824  oppggrpb  14827  invghm  15126  opprrngb  15410  abvn0b  16039  gzrngunit  16433  zrngunit  16434  dvdsrz  16436  zlmlmod  16473  zlmassa  16474  cygth  16521  frgpcyg  16523  tgclb  16704  iscldtop  16828  isnrm2  17082  isnrm3  17083  discmp  17121  dfcon2  17141  2ndcsb  17171  dis2ndc  17182  loclly  17209  iskgen2  17239  dfac14  17308  kqtop  17432  kqt0  17433  kqreg  17438  kqnrm  17439  hmpher  17471  hmphsymb  17473  hmph0  17482  kqhmph  17506  ist1-5lem  17507  elmptrab2  17519  isfil2  17547  filunirn  17573  isufil2  17599  hausflim  17672  isfcls  17700  alexsubALT  17741  istgp2  17770  xmetunirn  17898  dscmet  18091  dscopn  18092  isngp4  18129  zcld  18315  zlmclm  18589  iscmet2  18716  iundisj  18901  i1f1lem  19040  fta1b  19551  elply2  19574  elqaa  19698  aannenlem2  19705  wilth  20305  lgsne0  20568  2sqlem2  20599  ostth  20784  nmlno0lem  21365  isblo3i  21373  blocni  21377  hvsubeq0i  21638  hvaddcani  21640  bcseqi  21695  isch3  21817  norm1exi  21825  hhsssh  21842  shslubi  21960  dfch2  21982  pjoc1i  22006  pjchi  22007  shs00i  22025  chsscon3i  22036  chlejb1i  22051  chj00i  22062  shjshseli  22068  h1de2ctlem  22130  spanunsni  22154  cmcmi  22167  cmbr3i  22175  cmbr4i  22176  pj11i  22286  hosubeq0i  22402  dmadjrnb  22482  nmlnop0iALT  22571  lnopeq0i  22583  elunop2  22589  lnconi  22609  lncnopbd  22613  adjbdlnb  22660  adjbd1o  22661  adjeq0  22667  rnbra  22683  pjss1coi  22739  pjss2coi  22740  pjnormssi  22744  pjssdif2i  22750  pjssdif1i  22751  dfpjop  22758  pjinvari  22767  pjin2i  22769  pjci  22776  pjcmul1i  22777  pjcmul2i  22778  strb  22834  hstrbi  22842  mdsl1i  22897  atom1d  22929  chrelat2i  22941  cvbr4i  22943  cvexchi  22945  sumdmdi  22996  dmdbr4ati  22997  dmdbr5ati  22998  dmdbr6ati  22999  dmdbr7ati  23000  cdj3i  23017  ballotlem2  23043  ballotlemrinv  23088  wrdumgra  23275  nepss  23479  dfpo2  23518  dfon2  23552  distel  23564  elno2  23711  axbday  23732  elfix  23854  dffix2  23856  fnimage  23878  altopthsn  23905  mptelee  23933  ellines  24185  rankeq1o  24211  df3nandALT1  24245  wl-pm5.74lem  24327  and4as  24349  altdftru  24358  trcrm  24361  facrm  24363  bibox  24392  binxt  24394  nxtor  24395  nxtand  24396  bidia  24399  evpexun  24408  alalifal  24413  boxand  24416  axlll2  24438  dmoprabss6  24445  restidsing  24486  fixpc  24504  sssu  24552  dstr  24582  definc  24690  domncnt  24693  ranncnt  24694  dfps2  24700  sallnei  24940  altretop  25011  addcanri  25077  bisig0  25473  opnrebl2  25647  locfindis  25716  cover2  25769  isbnd3  25919  cntotbnd  25931  heibor  25956  isfld2  26041  isfldidl  26104  prtlem16  26148  funsnfsup  26173  ismrc  26187  isnacs3  26196  rexzrexnn0  26296  eldioph4b  26305  dford3  26532  wopprc  26534  ttac  26540  pw2f1ocnv  26541  dfac11  26571  dfac21  26575  isnumbasabl  26682  isnumbasgrp  26683  dfacbasgrp  26684  aaitgo  26778  pmtrfb  26817  pm10.55  26975  pm11.57  26999  sbeqalbi  27011  pm13.192  27021  pm13.194  27023  ipo0  27063  ifr0  27064  xpexb  27069  reuan  27349  afvfv0bi  27406  ffnafv  27424  com3rgbi  27559  pm2.43bgbi  27562  pm2.43cbi  27563  sb5ALT  27571  trsbc  27587  2pm13.193  27601  a9e2ndeq  27608  2uasbanh  27610  eelT01  27769  eel0T1  27770  uunT1  27835  zfregs2VD  27897  equncomVD  27924  trsbcVD  27933  undif3VD  27938  2pm13.193VD  27959  a9e2eqVD  27963  a9e2ndeqVD  27965  2uasbanhVD  27967  a9e2ndeqALT  27988  bnj1533  28163  bnj983  28262  equvinv  28393  equvelv  28395  isltrn2N  29588
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