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  1593  cbvexvw  1677  cbvex  1925  sb8e  2033  cbvrexf  2759  cbvrexcsf  3144  dfss4  3403  indifdir  3425  difprsn  3756  brdif  4071  pwundifOLD  4301  tfinds  4650  difopab  4817  rexiunxp  4826  rexxpf  4831  somin1  5079  cnvdif  5087  imadif  5327  brprcneu  5518  dffv2  5592  difxp  6153  poxp  6227  porpss  6281  tz7.48lem  6453  brsdom  6884  brsdom2  6985  fimax2g  7103  ordunifi  7107  dfsup2  7195  dfsup2OLD  7196  suc11reg  7320  rankxplim2  7550  rankxplim3  7551  alephval3  7737  kmlem4  7779  cflim2  7889  isfin4-2  7940  fin23lem25  7950  fin1a2lem5  8030  fin12  8039  axcclem  8083  zorng  8131  infinf  8188  alephadd  8199  fpwwe2  8265  axpre-lttri  8787  dfinfmr  9731  infmsup  9732  infmrgelb  9734  infmrlb  9735  arch  9962  rpneg  10383  xmulcom  10586  xmulneg1  10589  xmulf  10592  xrinfmss2  10629  difreicc  10767  hashfun  11389  incexc2  12297  fctop  16741  cctop  16743  ntreq0  16814  ordtbas2  16921  cmpcld  17129  hausdiag  17339  fbun  17535  fbfinnfr  17536  opnfbas  17537  fbasrn  17579  filuni  17580  ufinffr  17624  alexsubALTlem2  17742  ellogdm  19986  avril1  20836  shne0i  22027  chnlei  22064  cvnbtwn2  22867  cvnbtwn3  22868  cvnbtwn4  22869  chrelat2i  22945  atabs2i  22982  dmdbr5ati  23002  ballotlem2  23047  ballotlemodife  23056  ballotlem4  23057  ballotlemimin  23064  nmo  23144  cntnevol  23175  eliccelico  23270  elicoelioo  23271  xrdifh  23273  disjdifprg  23352  gsumpropd2lem  23379  hasheuni  23453  erdszelem9  23730  dftr6  24107  fundmpss  24122  dfon2lem5  24143  dfon2lem8  24146  dfon2lem9  24147  nodenselem7  24341  nocvxminlem  24344  symdifass  24371  dffun10  24453  elfuns  24454  tfrqfree  24489  df3nandALT1  24835  andnand1  24837  imnand2  24838  albineal  24999  evevifev  25014  gtinf  26234  fdc  26455  nninfnub  26461  n0el  26725  ctbnfien  26901  rencldnfilem  26903  numinfctb  27268  f1omvdco3  27392  psgnunilem4  27420  gsumcom3  27454  compab  27644  fmul01lt1lem2  27715  mpt2xopynvov0g  28080  uvtx01vtx  28164  zfregs2VD  28617  undif3VD  28658  onfrALTlem5VD  28661  bnj1143  28822  bnj1304  28852  bnj1476  28879  bnj1533  28884  bnj1174  29033  bnj1204  29042  bnj1280  29050  ax12-4  29106  lcvnbtwn2  29217  lcvnbtwn3  29218  cvrnbtwn3  29466  dalem18  29870  lhpocnel2  30208  cdleme0nex  30479  cdlemk19w  31161  dihglblem6  31530  dvh2dim  31635  dvh3dim3N  31639
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