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

Theorem notbii 289
Description: Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
notbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
notbii  |-  ( -. 
ph 
<->  -.  ps )

Proof of Theorem notbii
StepHypRef Expression
1 notbii.1 . 2  |-  ( ph  <->  ps )
2 notbi 288 . 2  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
31, 2mpbi 201 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178
This theorem is referenced by:  sylnbi  299  xchnxbi  301  xchbinx  303  oplem1  932  nancom  1300  xorcom  1317  xorass  1318  xorneg2  1322  xorbi12i  1324  trunanfal  1365  falxortru  1370  hadnot  1403  cadnot  1404  nic-axALT  1449  tbw-bijust  1473  rb-bijust  1524  19.43OLD  1618  cbvexvw  1720  hbn1fw  1722  excom  1759  cbvex  1987  cbvrexf  2936  cbvrexcsf  3301  dfss4  3563  indifdir  3585  difprsnss  3963  brdif  4291  tfinds  4874  difopab  5041  rexiunxp  5050  rexxpf  5055  somin1  5305  cnvdif  5313  imadif  5563  brprcneu  5756  dffv2  5832  difxp  6416  poxp  6494  porpss  6562  tz7.48lem  6734  brsdom  7166  brsdom2  7267  fimax2g  7389  ordunifi  7393  dfsup2  7483  dfsup2OLD  7484  suc11reg  7610  rankxplim2  7842  rankxplim3  7843  alephval3  8029  kmlem4  8071  cflim2  8181  isfin4-2  8232  fin23lem25  8242  fin1a2lem5  8322  fin12  8331  axcclem  8375  zorng  8422  infinf  8479  alephadd  8490  fpwwe2  8556  axpre-lttri  9078  dfinfmr  10023  infmsup  10024  infmrgelb  10026  infmrlb  10027  arch  10256  rpneg  10679  xmulcom  10883  xmulneg1  10886  xmulf  10889  xrinfmss2  10927  difreicc  11066  hashfun  11738  incexc2  12656  fctop  17106  cctop  17108  ntreq0  17179  ordtbas2  17293  cmpcld  17503  hausdiag  17715  fbun  17910  fbfinnfr  17911  opnfbas  17912  fbasrn  17954  filuni  17955  ufinffr  17999  alexsubALTlem2  18117  ellogdm  20568  usgraidx2v  21450  avril1  21795  shne0i  22988  chnlei  23025  cvnbtwn2  23828  cvnbtwn3  23829  cvnbtwn4  23830  chrelat2i  23906  atabs2i  23943  dmdbr5ati  23963  nmo  24009  disjdifprg  24052  eliccelico  24175  elicoelioo  24176  xrdifh  24178  tosglb  24227  xrnarchi  24289  hasheuni  24510  cntnevol  24617  sibfof  24689  ballotlem2  24781  ballotlemodife  24790  erdszelem9  24920  fzp1nel  25245  dftr6  25408  pocnv  25422  fundmpss  25425  dfon2lem5  25449  dfon2lem8  25452  dfon2lem9  25453  wzel  25610  nodenselem7  25677  nocvxminlem  25680  symdifass  25707  elfuns  25795  tfrqfree  25831  df3nandALT1  26181  andnand1  26183  imnand2  26184  gtinf  26364  fdc  26491  nninfnub  26497  notornotel2  26751  tsbi4  26760  ts3an2  26775  ts3an3  26776  ts3or1  26777  n0el  26820  ctbnfien  26991  rencldnfilem  26993  numinfctb  27357  f1omvdco3  27481  psgnunilem4  27509  gsumcom3  27543  compab  27732  otiunsndisj  28179  otiunsndisjX  28180  swrdccatin2  28342  2spotiundisj  28623  zfregs2VD  29127  undif3VD  29168  onfrALTlem5VD  29171  sineq0ALT  29223  bnj1143  29335  bnj1304  29365  bnj1476  29392  bnj1533  29397  bnj1174  29546  bnj1204  29555  bnj1280  29563  cbvexwAUX7  29694  sb8ewAUX7  29768  cbvexOLD7  29900  sbcomOLD7  29929  sb8eOLD7  29931  lcvnbtwn2  29999  lcvnbtwn3  30000  cvrnbtwn3  30248  dalem18  30652  lhpocnel2  30990  cdleme0nex  31261  cdlemk19w  31943  dihglblem6  32312  dvh2dim  32417  dvh3dim3N  32421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator