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

Theorem notbii 288
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 287 . 2  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
31, 2mpbi 200 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  sylnbi  298  xchnxbi  300  xchbinx  302  oplem1  931  nancom  1296  xorcom  1313  xorass  1314  xorneg2  1318  xorbi12i  1320  trunanfal  1361  falxortru  1366  hadnot  1399  cadnot  1400  nic-axALT  1445  tbw-bijust  1469  rb-bijust  1520  19.43OLD  1613  cbvexvw  1713  hbn1fw  1715  excom  1752  cbvex  2041  cbvrexf  2891  cbvrexcsf  3276  dfss4  3539  indifdir  3561  difprsnss  3898  brdif  4224  tfinds  4802  difopab  4969  rexiunxp  4978  rexxpf  4983  somin1  5233  cnvdif  5241  imadif  5491  brprcneu  5684  dffv2  5759  difxp  6343  poxp  6421  porpss  6489  tz7.48lem  6661  brsdom  7093  brsdom2  7194  fimax2g  7316  ordunifi  7320  dfsup2  7409  dfsup2OLD  7410  suc11reg  7534  rankxplim2  7764  rankxplim3  7765  alephval3  7951  kmlem4  7993  cflim2  8103  isfin4-2  8154  fin23lem25  8164  fin1a2lem5  8244  fin12  8253  axcclem  8297  zorng  8344  infinf  8401  alephadd  8412  fpwwe2  8478  axpre-lttri  9000  dfinfmr  9945  infmsup  9946  infmrgelb  9948  infmrlb  9949  arch  10178  rpneg  10601  xmulcom  10805  xmulneg1  10808  xmulf  10811  xrinfmss2  10849  difreicc  10988  hashfun  11659  incexc2  12577  fctop  17027  cctop  17029  ntreq0  17100  ordtbas2  17213  cmpcld  17423  hausdiag  17634  fbun  17829  fbfinnfr  17830  opnfbas  17831  fbasrn  17873  filuni  17874  ufinffr  17918  alexsubALTlem2  18036  ellogdm  20487  usgraidx2v  21369  avril1  21714  shne0i  22907  chnlei  22944  cvnbtwn2  23747  cvnbtwn3  23748  cvnbtwn4  23749  chrelat2i  23825  atabs2i  23862  dmdbr5ati  23882  nmo  23930  disjdifprg  23974  eliccelico  24097  elicoelioo  24098  xrdifh  24100  tosglb  24149  xrnarchi  24211  hasheuni  24432  cntnevol  24539  sibfof  24611  ballotlem2  24703  ballotlemodife  24712  erdszelem9  24842  fzp1nel  25167  dftr6  25325  fundmpss  25340  dfon2lem5  25361  dfon2lem8  25364  dfon2lem9  25365  nodenselem7  25559  nocvxminlem  25562  symdifass  25589  dffun10  25671  elfuns  25672  tfrqfree  25708  df3nandALT1  26054  andnand1  26056  imnand2  26057  gtinf  26216  fdc  26343  nninfnub  26349  n0el  26602  ctbnfien  26773  rencldnfilem  26775  numinfctb  27140  f1omvdco3  27264  psgnunilem4  27292  gsumcom3  27326  compab  27515  otiunsndisj  27958  otiunsndisjX  27959  2spotiundisj  28169  zfregs2VD  28666  undif3VD  28707  onfrALTlem5VD  28710  bnj1143  28871  bnj1304  28901  bnj1476  28928  bnj1533  28933  bnj1174  29082  bnj1204  29091  bnj1280  29099  cbvexwAUX7  29228  sb8ewAUX7  29299  cbvexOLD7  29414  sbcomOLD7  29443  sb8eOLD7  29445  lcvnbtwn2  29514  lcvnbtwn3  29515  cvrnbtwn3  29763  dalem18  30167  lhpocnel2  30505  cdleme0nex  30776  cdlemk19w  31458  dihglblem6  31827  dvh2dim  31932  dvh3dim3N  31936
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 178
  Copyright terms: Public domain W3C validator