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

Theorem notbii 288
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 287 . 2  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
31, 2mpbi 200 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  sylnbi  298  xchnxbi  300  xchbinx  302  oplem1  931  nancom  1299  xorcom  1316  xorass  1317  xorneg2  1321  xorbi12i  1323  trunanfal  1364  falxortru  1369  hadnot  1402  cadnot  1403  nic-axALT  1448  tbw-bijust  1472  rb-bijust  1523  19.43OLD  1616  cbvexvw  1717  hbn1fw  1719  excom  1756  cbvex  1983  cbvrexf  2927  cbvrexcsf  3312  dfss4  3575  indifdir  3597  difprsnss  3934  brdif  4260  tfinds  4839  difopab  5006  rexiunxp  5015  rexxpf  5020  somin1  5270  cnvdif  5278  imadif  5528  brprcneu  5721  dffv2  5796  difxp  6380  poxp  6458  porpss  6526  tz7.48lem  6698  brsdom  7130  brsdom2  7231  fimax2g  7353  ordunifi  7357  dfsup2  7447  dfsup2OLD  7448  suc11reg  7574  rankxplim2  7804  rankxplim3  7805  alephval3  7991  kmlem4  8033  cflim2  8143  isfin4-2  8194  fin23lem25  8204  fin1a2lem5  8284  fin12  8293  axcclem  8337  zorng  8384  infinf  8441  alephadd  8452  fpwwe2  8518  axpre-lttri  9040  dfinfmr  9985  infmsup  9986  infmrgelb  9988  infmrlb  9989  arch  10218  rpneg  10641  xmulcom  10845  xmulneg1  10848  xmulf  10851  xrinfmss2  10889  difreicc  11028  hashfun  11700  incexc2  12618  fctop  17068  cctop  17070  ntreq0  17141  ordtbas2  17255  cmpcld  17465  hausdiag  17677  fbun  17872  fbfinnfr  17873  opnfbas  17874  fbasrn  17916  filuni  17917  ufinffr  17961  alexsubALTlem2  18079  ellogdm  20530  usgraidx2v  21412  avril1  21757  shne0i  22950  chnlei  22987  cvnbtwn2  23790  cvnbtwn3  23791  cvnbtwn4  23792  chrelat2i  23868  atabs2i  23905  dmdbr5ati  23925  nmo  23973  disjdifprg  24017  eliccelico  24140  elicoelioo  24141  xrdifh  24143  tosglb  24192  xrnarchi  24254  hasheuni  24475  cntnevol  24582  sibfof  24654  ballotlem2  24746  ballotlemodife  24755  erdszelem9  24885  fzp1nel  25210  dftr6  25373  pocnv  25387  fundmpss  25390  dfon2lem5  25414  dfon2lem8  25417  dfon2lem9  25418  wzel  25575  nodenselem7  25642  nocvxminlem  25645  symdifass  25672  elfuns  25760  tfrqfree  25796  df3nandALT1  26146  andnand1  26148  imnand2  26149  gtinf  26322  fdc  26449  nninfnub  26455  n0el  26708  ctbnfien  26879  rencldnfilem  26881  numinfctb  27245  f1omvdco3  27369  psgnunilem4  27397  gsumcom3  27431  compab  27620  otiunsndisj  28066  otiunsndisjX  28067  swrdccatin2  28210  2spotiundisj  28451  zfregs2VD  28953  undif3VD  28994  onfrALTlem5VD  28997  sineq0ALT  29049  bnj1143  29161  bnj1304  29191  bnj1476  29218  bnj1533  29223  bnj1174  29372  bnj1204  29381  bnj1280  29389  cbvexwAUX7  29520  sb8ewAUX7  29594  cbvexOLD7  29726  sbcomOLD7  29755  sb8eOLD7  29757  lcvnbtwn2  29825  lcvnbtwn3  29826  cvrnbtwn3  30074  dalem18  30478  lhpocnel2  30816  cdleme0nex  31087  cdlemk19w  31769  dihglblem6  32138  dvh2dim  32243  dvh3dim3N  32247
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 178
  Copyright terms: Public domain W3C validator