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

Theorem notbii 289
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 288 . 2  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
31, 2mpbi 201 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178
This theorem is referenced by:  sylnbi  299  xchnxbi  301  xchbinx  303  oplem1  935  nancom  1295  xorcom  1303  xorass  1304  xorneg2  1308  xorbi12i  1310  trunanfal  1351  falxortru  1356  hadnot  1389  cadnot  1390  nic-axALT  1434  tbw-bijust  1458  rb-bijust  1509  19.43OLD  1605  cbvex  1877  sb8e  1987  cbvrexf  2704  cbvrexcsf  3072  dfss4  3310  indifdir  3332  difprsn  3658  brdif  3968  pwundifOLD  4194  tfinds  4541  difopab  4724  rexiunxp  4733  rexxpf  4738  somin1  4986  cnvdif  4994  imadif  5184  dffv2  5444  difxp  6005  poxp  6079  porpss  6133  tz7.48lem  6339  brsdom  6770  brsdom2  6870  fimax2g  6988  ordunifi  6992  dfsup2  7079  dfsup2OLD  7080  suc11reg  7204  rankxplim2  7434  rankxplim3  7435  alephval3  7621  kmlem4  7663  cflim2  7773  isfin4-2  7824  fin23lem25  7834  fin1a2lem5  7914  fin12  7923  axcclem  7967  zorng  8015  alephadd  8079  fpwwe2  8145  axpre-lttri  8667  dfinfmr  9611  infmsup  9612  infmrgelb  9614  infmrlb  9615  arch  9841  rpneg  10262  xmulcom  10464  xmulneg1  10467  xmulf  10470  xrinfmss2  10507  difreicc  10645  hashfun  11266  fctop  16573  cctop  16575  ntreq0  16646  ordtbas2  16753  cmpcld  16961  hausdiag  17171  fbun  17367  fbfinnfr  17368  opnfbas  17369  fbasrn  17411  filuni  17412  ufinffr  17456  alexsubALTlem2  17574  ellogdm  19818  avril1  20666  shne0i  21857  chnlei  21894  cvnbtwn2  22697  cvnbtwn3  22698  cvnbtwn4  22699  chrelat2i  22775  atabs2i  22812  dmdbr5ati  22832  erdszelem9  22901  dftr6  23277  fundmpss  23290  dfon2lem5  23311  dfon2lem8  23314  dfon2lem9  23315  axdenselem7  23509  nocvxminlem  23512  axfelem22  23535  symdifass  23546  tfrqfree  23663  df3nandALT1  24009  andnand1  24011  imnand2  24012  albineal  24164  evevifev  24179  gtinf  25400  fdc  25621  nninfnub  25627  n0el  25891  ctbnfien  26067  rencldnfilem  26069  numinfctb  26434  f1omvdco3  26558  psgnunilem4  26586  gsumcom3  26620  compab  26811  zfregs2VD  27307  undif3VD  27348  onfrALTlem5VD  27351  bnj1143  27511  bnj1304  27541  bnj1476  27568  bnj1533  27573  bnj1174  27722  bnj1204  27731  bnj1280  27739  ax12-4  27795  lcvnbtwn2  27906  lcvnbtwn3  27907  cvrnbtwn3  28155  dalem18  28559  lhpocnel2  28897  cdleme0nex  29168  cdlemk19w  29850  dihglblem6  30219  dvh2dim  30324  dvh3dim3N  30328
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator