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  1298  xorass  1299  xorneg2  1303  xorbi12i  1305  trunanfal  1345  falxortru  1350  hadnot  1383  cadnot  1384  nic-axALT  1429  tbw-bijust  1453  rb-bijust  1504  19.43OLD  1595  cbvexvw  1679  cbvex  1927  sb8e  2035  cbvrexf  2761  cbvrexcsf  3146  dfss4  3405  indifdir  3427  difprsn  3758  brdif  4073  pwundifOLD  4303  tfinds  4652  difopab  4819  rexiunxp  4828  rexxpf  4833  somin1  5081  cnvdif  5089  imadif  5329  brprcneu  5520  dffv2  5594  difxp  6155  poxp  6229  porpss  6283  tz7.48lem  6455  brsdom  6886  brsdom2  6987  fimax2g  7105  ordunifi  7109  dfsup2  7197  dfsup2OLD  7198  suc11reg  7322  rankxplim2  7552  rankxplim3  7553  alephval3  7739  kmlem4  7781  cflim2  7891  isfin4-2  7942  fin23lem25  7952  fin1a2lem5  8032  fin12  8041  axcclem  8085  zorng  8133  infinf  8190  alephadd  8201  fpwwe2  8267  axpre-lttri  8789  dfinfmr  9733  infmsup  9734  infmrgelb  9736  infmrlb  9737  arch  9964  rpneg  10385  xmulcom  10588  xmulneg1  10591  xmulf  10594  xrinfmss2  10631  difreicc  10769  hashfun  11391  incexc2  12299  fctop  16743  cctop  16745  ntreq0  16816  ordtbas2  16923  cmpcld  17131  hausdiag  17341  fbun  17537  fbfinnfr  17538  opnfbas  17539  fbasrn  17581  filuni  17582  ufinffr  17626  alexsubALTlem2  17744  ellogdm  19988  avril1  20838  shne0i  22029  chnlei  22066  cvnbtwn2  22869  cvnbtwn3  22870  cvnbtwn4  22871  chrelat2i  22947  atabs2i  22984  dmdbr5ati  23004  ballotlem2  23049  ballotlemodife  23058  ballotlem4  23059  ballotlemimin  23066  nmo  23146  cntnevol  23177  eliccelico  23272  elicoelioo  23273  xrdifh  23275  disjdifprg  23354  gsumpropd2lem  23381  hasheuni  23455  erdszelem9  23732  dftr6  24109  fundmpss  24124  dfon2lem5  24145  dfon2lem8  24148  dfon2lem9  24149  nodenselem7  24343  nocvxminlem  24346  symdifass  24373  dffun10  24455  elfuns  24456  tfrqfree  24491  df3nandALT1  24837  andnand1  24839  imnand2  24840  albineal  25010  evevifev  25025  gtinf  26245  fdc  26466  nninfnub  26472  n0el  26736  ctbnfien  26912  rencldnfilem  26914  numinfctb  27279  f1omvdco3  27403  psgnunilem4  27431  gsumcom3  27465  compab  27655  fmul01lt1lem2  27726  mpt2xopynvov0g  28091  uvtx01vtx  28175  zfregs2VD  28690  undif3VD  28731  onfrALTlem5VD  28734  bnj1143  28895  bnj1304  28925  bnj1476  28952  bnj1533  28957  bnj1174  29106  bnj1204  29115  bnj1280  29123  ax12-4  29179  lcvnbtwn2  29290  lcvnbtwn3  29291  cvrnbtwn3  29539  dalem18  29943  lhpocnel2  30281  cdleme0nex  30552  cdlemk19w  31234  dihglblem6  31603  dvh2dim  31708  dvh3dim3N  31712
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