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

Theorem notbii 287
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 286 . 2  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
31, 2mpbi 199 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  sylnbi  297  xchnxbi  299  xchbinx  301  oplem1  930  nancom  1295  xorcom  1312  xorass  1313  xorneg2  1317  xorbi12i  1319  trunanfal  1360  falxortru  1365  hadnot  1398  cadnot  1399  nic-axALT  1444  tbw-bijust  1468  rb-bijust  1519  19.43OLD  1611  cbvexvw  1708  excom  1746  cbvex  1998  cbvrexf  2844  cbvrexcsf  3230  dfss4  3491  indifdir  3513  difprsnss  3849  brdif  4173  pwundifOLD  4403  tfinds  4753  difopab  4920  rexiunxp  4929  rexxpf  4934  somin1  5182  cnvdif  5190  imadif  5432  brprcneu  5625  dffv2  5699  difxp  6280  poxp  6355  mpt2xopynvov0g  6362  porpss  6423  tz7.48lem  6595  brsdom  7027  brsdom2  7128  fimax2g  7250  ordunifi  7254  dfsup2  7342  dfsup2OLD  7343  suc11reg  7467  rankxplim2  7697  rankxplim3  7698  alephval3  7884  kmlem4  7926  cflim2  8036  isfin4-2  8087  fin23lem25  8097  fin1a2lem5  8177  fin12  8186  axcclem  8230  zorng  8278  infinf  8335  alephadd  8346  fpwwe2  8412  axpre-lttri  8934  dfinfmr  9878  infmsup  9879  infmrgelb  9881  infmrlb  9882  arch  10111  rpneg  10534  xmulcom  10738  xmulneg1  10741  xmulf  10744  xrinfmss2  10782  difreicc  10920  hashfun  11587  incexc2  12505  fctop  16958  cctop  16960  ntreq0  17031  ordtbas2  17138  cmpcld  17346  hausdiag  17556  fbun  17748  fbfinnfr  17749  opnfbas  17750  fbasrn  17792  filuni  17793  ufinffr  17837  alexsubALTlem2  17955  ellogdm  20208  usgraidx2v  21089  avril1  21147  shne0i  22340  chnlei  22377  cvnbtwn2  23180  cvnbtwn3  23181  cvnbtwn4  23182  chrelat2i  23258  atabs2i  23295  dmdbr5ati  23315  nmo  23367  disjdifprg  23415  eliccelico  23541  elicoelioo  23542  xrdifh  23544  gsumpropd2lem  23611  hasheuni  23940  cntnevol  24045  ballotlem2  24194  ballotlemodife  24203  ballotlem4  24204  ballotlemimin  24211  erdszelem9  24333  fzp1nel  24694  gamma1  24828  dftr6  24848  fundmpss  24863  dfon2lem5  24884  dfon2lem8  24887  dfon2lem9  24888  nodenselem7  25082  nocvxminlem  25085  symdifass  25112  dffun10  25194  elfuns  25195  tfrqfree  25231  df3nandALT1  25577  andnand1  25579  imnand2  25580  gtinf  25741  fdc  25962  nninfnub  25968  n0el  26231  ctbnfien  26407  rencldnfilem  26409  numinfctb  26774  f1omvdco3  26898  psgnunilem4  26926  gsumcom3  26960  compab  27150  fmul01lt1lem2  27221  cusgrasizeindslem2  27639  uvtx01vtx  27657  frgrawopreglem4  27882  zfregs2VD  28381  undif3VD  28422  onfrALTlem5VD  28425  bnj1143  28586  bnj1304  28616  bnj1476  28643  bnj1533  28648  bnj1174  28797  bnj1204  28806  bnj1280  28814  cbvexwAUX7  28943  sb8ewAUX7  29014  cbvexOLD7  29129  sbcomOLD7  29158  sb8eOLD7  29160  ax12-4  29177  lcvnbtwn2  29288  lcvnbtwn3  29289  cvrnbtwn3  29537  dalem18  29941  lhpocnel2  30279  cdleme0nex  30550  cdlemk19w  31232  dihglblem6  31601  dvh2dim  31706  dvh3dim3N  31710
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