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  1290  xorcom  1307  xorass  1308  xorneg2  1312  xorbi12i  1314  trunanfal  1355  falxortru  1360  hadnot  1393  cadnot  1394  nic-axALT  1439  tbw-bijust  1463  rb-bijust  1514  19.43OLD  1606  cbvexvw  1703  excom  1741  cbvex  1990  cbvrexf  2835  cbvrexcsf  3220  dfss4  3479  indifdir  3501  difprsnss  3832  brdif  4152  pwundifOLD  4382  tfinds  4732  difopab  4899  rexiunxp  4908  rexxpf  4913  somin1  5161  cnvdif  5169  imadif  5409  brprcneu  5601  dffv2  5675  difxp  6240  poxp  6314  porpss  6368  tz7.48lem  6540  brsdom  6972  brsdom2  7073  fimax2g  7193  ordunifi  7197  dfsup2  7285  dfsup2OLD  7286  suc11reg  7410  rankxplim2  7640  rankxplim3  7641  alephval3  7827  kmlem4  7869  cflim2  7979  isfin4-2  8030  fin23lem25  8040  fin1a2lem5  8120  fin12  8129  axcclem  8173  zorng  8221  infinf  8278  alephadd  8289  fpwwe2  8355  axpre-lttri  8877  dfinfmr  9821  infmsup  9822  infmrgelb  9824  infmrlb  9825  arch  10054  rpneg  10475  xmulcom  10678  xmulneg1  10681  xmulf  10684  xrinfmss2  10721  difreicc  10859  hashfun  11485  incexc2  12394  fctop  16847  cctop  16849  ntreq0  16920  ordtbas2  17027  cmpcld  17235  hausdiag  17445  fbun  17637  fbfinnfr  17638  opnfbas  17639  fbasrn  17681  filuni  17682  ufinffr  17726  alexsubALTlem2  17844  ellogdm  20097  avril1  20948  shne0i  22141  chnlei  22178  cvnbtwn2  22981  cvnbtwn3  22982  cvnbtwn4  22983  chrelat2i  23059  atabs2i  23096  dmdbr5ati  23116  nmo  23168  disjdifprg  23216  eliccelico  23342  elicoelioo  23343  xrdifh  23345  gsumpropd2lem  23412  hasheuni  23741  cntnevol  23846  ballotlem2  23995  ballotlemodife  24004  ballotlem4  24005  ballotlemimin  24012  erdszelem9  24134  fzp1nel  24511  gamma1  24645  dftr6  24665  fundmpss  24680  dfon2lem5  24701  dfon2lem8  24704  dfon2lem9  24705  nodenselem7  24899  nocvxminlem  24902  symdifass  24929  dffun10  25011  elfuns  25012  tfrqfree  25048  df3nandALT1  25394  andnand1  25396  imnand2  25397  gtinf  25558  fdc  25779  nninfnub  25785  n0el  26048  ctbnfien  26224  rencldnfilem  26226  numinfctb  26591  f1omvdco3  26715  psgnunilem4  26743  gsumcom3  26777  compab  26967  fmul01lt1lem2  27038  mpt2xopynvov0g  27437  usgraidx2v  27566  cusgrasizeindslem2  27637  uvtx01vtx  27655  frgrawopreglem4  27880  zfregs2VD  28379  undif3VD  28420  onfrALTlem5VD  28423  bnj1143  28584  bnj1304  28614  bnj1476  28641  bnj1533  28646  bnj1174  28795  bnj1204  28804  bnj1280  28812  cbvexwAUX7  28941  sb8ewAUX7  29012  cbvexOLD7  29127  sbcomOLD7  29156  sb8eOLD7  29158  ax12-4  29175  lcvnbtwn2  29286  lcvnbtwn3  29287  cvrnbtwn3  29535  dalem18  29939  lhpocnel2  30277  cdleme0nex  30548  cdlemk19w  31230  dihglblem6  31599  dvh2dim  31704  dvh3dim3N  31708
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