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

Theorem impbii 182
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 181 . 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 178
This theorem is referenced by:  dfbi1  186  bicom  193  biid  229  2th  232  pm5.74  237  bitri  242  notnot  284  con34b  285  notbi  288  bibi2i  306  con1b  325  con2b  326  bi2.04  352  pm5.4  353  imdi  354  pm4.8  356  pm4.81  357  orcom  378  dfor2  402  impexp  435  ancom  439  oridm  502  orbi2i  507  or12  511  pm4.45im  547  pm4.44  562  pm4.79  568  anass  632  jaob  760  jcab  835  andi  839  pm4.72  848  oibabs  853  pm4.82  896  consensus  927  rnlem  933  3jaob  1247  truan  1341  dfnot  1342  3impexp  1376  3impexpbicom  1377  cad1  1408  tbw-bijust  1473  tbw-negdf  1474  19.26  1604  sbbii  1666  19.9v  1677  equcom  1693  19.3vOLD  1710  cbvalw  1715  cbvalvwOLD  1717  alcom  1753  19.3  1792  19.9hOLD  1796  19.23hOLD  1840  equsalhwOLD  1862  19.21hOLD  1863  excomOLD  1883  19.41  1901  19.41OLD  1902  cbval  1983  equsalOLD  2001  equsex  2003  ax12olem1  2006  ax12olem1OLD  2012  ax12olem3OLD  2014  equvin  2088  equs45f  2089  dfsb2  2110  sb6f  2124  sbnOLD  2133  sbim  2137  sb5rf  2168  sb6rf  2169  sb9  2173  mo  2305  eu2  2308  mo2  2312  exmoeu  2325  euan  2340  2mo  2361  2eu6  2368  axext4  2422  cleqh  2535  nebi  2677  r19.26  2840  ralcom3  2875  ceqsex  2992  gencbvex  3000  gencbvex2  3001  eqvinc  3065  pm13.183  3078  rr19.3v  3079  rr19.28v  3080  euxfr2  3121  reu6  3125  reu3  3126  sbnfc2  3311  sspss  3448  unineq  3593  uneqin  3594  undif3  3604  difrab  3617  un00  3665  ssdifeq0  3712  r19.2zb  3720  ralf0  3736  elpr2  3835  snidb  3842  tppreqb  3941  difsnb  3942  pwpw0  3948  sssn  3959  preq12b  3976  preqsn  3982  pwsnALT  4012  unissint  4076  uniintsn  4089  iununi  4177  intex  4358  intnex  4359  iin0  4375  axpweq  4378  nfcvb  4396  sspwb  4415  unipw  4416  opnz  4434  opth  4437  opthwiener  4460  ssopab2b  4483  pwssun  4491  elon2  4594  unexb  4711  eusvnfb  4721  eusv2nf  4723  ralxfrALT  4744  uniexb  4754  iunpw  4761  ordeleqon  4771  onintrab  4783  unon  4813  onuninsuci  4822  ordzsl  4827  onzsl  4828  opelxp  4910  opthprc  4927  relop  5025  issetid  5029  xpid11  5093  elres  5183  iss  5191  issref  5249  asymref2  5253  xpnz  5294  ssrnres  5311  dfrel2  5323  relrelss  5395  unixp0  5405  fn0  5566  funssxp  5606  f00  5630  dffo2  5659  ffoss  5709  f1o00  5712  fo00  5713  fv3  5746  dffn5  5774  dff2  5883  dff3  5884  dffo4  5887  dffo5  5888  exfo  5889  fmpt  5892  ffnfv  5896  fsn  5908  fsn2  5910  fconstfv  5956  isores1  6056  ssoprab2b  6133  eqfnov2  6179  1st2ndb  6389  reldmtpos  6489  riotaundb  6593  abianfp  6718  omopthi  6902  mapsn  7057  mapsncnv  7062  mptelixpg  7101  elixpsn  7103  ixpsnf1o  7104  bren2  7140  en0  7172  en1  7176  en1b  7177  sbthb  7230  canth2  7262  onfin2  7300  sdom1  7310  1sdom  7313  fineqv  7326  unfilem1  7373  fiint  7385  pwfi  7404  unifpw  7411  wofib  7516  sucprcreg  7569  opthreg  7575  suc11reg  7576  infeq5  7594  rankwflemb  7721  r1elss  7734  pwwf  7735  unwf  7738  uniwf  7747  rankonid  7757  rankr1id  7790  rankuni  7791  rankxplim3  7807  scott0  7812  karden  7821  isnum3  7843  oncard  7849  card1  7857  cardlim  7861  cardmin2  7887  pm54.43lem  7888  ween  7918  acnnum  7935  alephsuc2  7963  alephgeom  7965  iscard3  7976  dfac3  8004  dfac4  8005  dfac5lem3  8008  dfac5  8011  dfac2  8013  dfac8  8017  dfac9  8018  dfacacn  8023  dfac13  8024  dfac12r  8028  dfac12k  8029  kmlem2  8033  kmlem13  8044  cdainf  8074  ackbij2  8125  cflim2  8145  isfin4-2  8196  isfin4-3  8197  isf33lem  8248  compsscnv  8253  fin1a2lem6  8287  domtriom  8325  ac9  8365  ac9s  8375  fodomb  8406  brdom3  8408  brdom5  8409  brdom4  8410  brdom7disj  8411  brdom6disj  8412  iunfo  8416  sdomsdomcard  8437  gch2  8556  gch3  8557  eltsk2g  8628  grutsk  8699  grothpw  8703  ordpipq  8821  ltbtwnnq  8857  mappsrpr  8985  map2psrpr  8987  elreal2  9009  le2tri3i  9205  ltadd2i  9206  elnn0nn  10264  elnnnn0b  10266  elnnnn0c  10267  elnnz  10294  elnn0z  10296  elz2  10300  elnnz1  10309  eluz2b2  10550  elnn1uz2  10554  elioo4g  10973  eluzfz2b  11068  fzn0  11072  elfz1end  11083  fzass4  11092  nn0fz0  11116  fzolb  11147  fzon0  11158  elfzo0  11173  elfzo1  11175  om2uzrani  11294  nn0opthi  11565  hashkf  11622  hashprb  11670  hashf1  11708  wrdexb  11765  sqr0lem  12048  rexanuz  12151  rexuz3  12154  fsum0diag  12563  sadcp1  12969  isprm6  13111  4sqlem4  13322  mreunirn  13828  isdrs2  14398  isacs5  14600  isacs4  14601  isacs3  14602  isnsg3  14976  gicer  15065  oppgmndb  15153  oppggrpb  15156  invghm  15455  opprrngb  15739  abvn0b  16364  gzrngunit  16766  zrngunit  16767  dvdsrz  16769  zlmlmod  16806  zlmassa  16807  cygth  16854  frgpcyg  16856  tgclb  17037  iscldtop  17161  isnrm2  17424  isnrm3  17425  discmp  17463  dfcon2  17484  2ndcsb  17514  dis2ndc  17525  loclly  17552  iskgen2  17582  dfac14  17652  kqtop  17779  kqt0  17780  kqreg  17785  kqnrm  17786  hmpher  17818  hmphsymb  17820  hmph0  17829  kqhmph  17853  ist1-5lem  17854  elmptrab2  17862  isfil2  17890  filunirn  17916  isufil2  17942  hausflim  18015  isfcls  18043  alexsubALT  18084  istgp2  18123  ustbas  18259  xmetunirn  18369  dscmet  18622  dscopn  18623  isngp4  18660  zcld  18846  zlmclm  19122  iscmet2  19249  iundisj  19444  i1f1lem  19583  fta1b  20094  elply2  20117  elqaa  20241  aannenlem2  20248  wilth  20856  lgsne0  21119  2sqlem2  21150  ostth  21335  uhgra0v  21347  wrdumgra  21353  usgra0v  21393  uvtx01vtx  21503  istrl2  21540  isspthonpth  21586  nmlno0lem  22296  isblo3i  22304  blocni  22308  hvsubeq0i  22567  hvaddcani  22569  bcseqi  22624  isch3  22746  norm1exi  22754  hhsssh  22771  shslubi  22889  dfch2  22911  pjoc1i  22935  pjchi  22936  shs00i  22954  chsscon3i  22965  chlejb1i  22980  chj00i  22991  shjshseli  22997  h1de2ctlem  23059  spanunsni  23083  cmcmi  23096  cmbr3i  23104  cmbr4i  23105  pj11i  23215  hosubeq0i  23331  dmadjrnb  23411  nmlnop0iALT  23500  lnopeq0i  23512  elunop2  23518  lnconi  23538  lncnopbd  23542  adjbdlnb  23589  adjbd1o  23590  adjeq0  23596  rnbra  23612  pjss1coi  23668  pjss2coi  23669  pjnormssi  23673  pjssdif2i  23679  pjssdif1i  23680  dfpjop  23687  pjinvari  23696  pjin2i  23698  pjci  23705  pjcmul1i  23706  pjcmul2i  23707  strb  23763  hstrbi  23771  mdsl1i  23826  atom1d  23858  chrelat2i  23870  cvbr4i  23872  cvexchi  23874  sumdmdi  23925  dmdbr4ati  23926  dmdbr5ati  23927  dmdbr6ati  23928  dmdbr7ati  23929  cdj3i  23946  difeq  24000  iundisjf  24031  iundisjfi  24154  xrge0tsmsbi  24226  issgon  24508  measbasedom  24558  ballotlem2  24748  ballotlemrinv  24793  nepss  25177  fprod0diag  25312  dfpo2  25380  dfon2  25421  distel  25433  elno2  25611  bdayfo  25632  fnimage  25776  altopthsn  25808  mptelee  25836  ellines  26088  rankeq1o  26114  df3nandALT1  26148  wl-pm5.74lem  26229  wl-nfnbi  26235  wl-exeq  26236  wl-aleq  26237  volsupnfl  26253  opnrebl2  26326  locfindis  26387  cover2  26417  isbnd3  26495  cntotbnd  26507  heibor  26532  isfld2  26617  isfldidl  26680  prtlem16  26720  funsnfsup  26745  ismrc  26757  isnacs3  26766  rexzrexnn0  26866  eldioph4b  26874  dford3  27101  wopprc  27103  ttac  27109  pw2f1ocnv  27110  dfac11  27139  dfac21  27143  isnumbasabl  27250  isnumbasgrp  27251  dfacbasgrp  27252  aaitgo  27346  pmtrfb  27385  pm10.55  27543  pm11.57  27567  sbeqalbi  27579  pm13.192  27589  pm13.194  27591  ipo0  27630  ifr0  27631  xpexb  27636  reuan  27936  afvfv0bi  27994  ffnafv  28013  f0bi  28080  fzo1fzo0n0  28139  usg2spthonot1  28410  frgra0v  28445  com3rgbi  28659  pm2.43bgbi  28662  pm2.43cbi  28663  sb5ALT  28671  trsbc  28687  2pm13.193  28701  a9e2ndeq  28708  2uasbanh  28710  eelT01  28880  eel0T1  28881  uunT1  28954  zfregs2VD  29015  equncomVD  29042  trsbcVD  29051  undif3VD  29056  2pm13.193VD  29077  a9e2eqVD  29081  a9e2ndeqVD  29083  2uasbanhVD  29085  a9e2ndeqALT  29105  bnj1533  29285  bnj983  29384  alcomwAUX7  29506  ax12olem3aAUX7  29519  equsalNEW7  29549  cbvalwwAUX7  29581  equvinNEW7  29591  sbnNEW7  29624  sbimNEW7  29627  sb5rfNEW7  29653  sb6rfNEW7  29654  sb8wAUX7  29655  equs45fNEW7  29683  sb6fNEW7  29695  dfsb2NEW7  29700  alcomw9bAUX7  29723  alcomOLD7  29743  excomOLD7  29756  cbvalOLD7  29787  nfsb4tw2AUXOLD7  29808  sbcomOLD7  29817  sb8OLD7  29818  sb9iOLD7  29820  sb9OLD7  29821  isltrn2N  30979
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 179
  Copyright terms: Public domain W3C validator