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  1878  sb8e  1988  cbvrexf  2734  cbvrexcsf  3119  dfss4  3378  indifdir  3400  difprsn  3730  brdif  4045  pwundifOLD  4273  tfinds  4622  difopab  4805  rexiunxp  4814  rexxpf  4819  somin1  5067  cnvdif  5075  imadif  5265  dffv2  5526  difxp  6087  poxp  6161  porpss  6215  tz7.48lem  6421  brsdom  6852  brsdom2  6953  fimax2g  7071  ordunifi  7075  dfsup2  7163  dfsup2OLD  7164  suc11reg  7288  rankxplim2  7518  rankxplim3  7519  alephval3  7705  kmlem4  7747  cflim2  7857  isfin4-2  7908  fin23lem25  7918  fin1a2lem5  7998  fin12  8007  axcclem  8051  zorng  8099  infinf  8156  alephadd  8167  fpwwe2  8233  axpre-lttri  8755  dfinfmr  9699  infmsup  9700  infmrgelb  9702  infmrlb  9703  arch  9930  rpneg  10351  xmulcom  10553  xmulneg1  10556  xmulf  10559  xrinfmss2  10596  difreicc  10734  hashfun  11355  fctop  16704  cctop  16706  ntreq0  16777  ordtbas2  16884  cmpcld  17092  hausdiag  17302  fbun  17498  fbfinnfr  17499  opnfbas  17500  fbasrn  17542  filuni  17543  ufinffr  17587  alexsubALTlem2  17705  ellogdm  19949  avril1  20797  shne0i  21988  chnlei  22025  cvnbtwn2  22828  cvnbtwn3  22829  cvnbtwn4  22830  chrelat2i  22906  atabs2i  22943  dmdbr5ati  22963  ballotlem2  23009  ballotlemodife  23018  ballotlem4  23019  ballotlemimin  23026  erdszelem9  23103  dftr6  23479  fundmpss  23492  dfon2lem5  23513  dfon2lem8  23516  dfon2lem9  23517  axdenselem7  23711  nocvxminlem  23714  axfelem22  23737  symdifass  23748  tfrqfree  23865  df3nandALT1  24211  andnand1  24213  imnand2  24214  albineal  24366  evevifev  24381  gtinf  25602  fdc  25823  nninfnub  25829  n0el  26093  ctbnfien  26269  rencldnfilem  26271  numinfctb  26636  f1omvdco3  26760  psgnunilem4  26788  gsumcom3  26822  compab  27013  fmul01lt1lem2  27084  zfregs2VD  27750  undif3VD  27791  onfrALTlem5VD  27794  bnj1143  27954  bnj1304  27984  bnj1476  28011  bnj1533  28016  bnj1174  28165  bnj1204  28174  bnj1280  28182  cbvexvK  28263  ax12o10lem5K  28288  ax12-4  28356  lcvnbtwn2  28467  lcvnbtwn3  28468  cvrnbtwn3  28716  dalem18  29120  lhpocnel2  29458  cdleme0nex  29729  cdlemk19w  30411  dihglblem6  30780  dvh2dim  30885  dvh3dim3N  30889
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