MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notbii 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  1296  xorcom  1313  xorass  1314  xorneg2  1318  xorbi12i  1320  trunanfal  1361  falxortru  1366  hadnot  1399  cadnot  1400  nic-axALT  1445  tbw-bijust  1469  rb-bijust  1520  19.43OLD  1613  cbvexvw  1713  hbn1fw  1715  excom  1752  cbvex  2060  cbvrexf  2895  cbvrexcsf  3280  dfss4  3543  indifdir  3565  difprsnss  3902  brdif  4228  tfinds  4806  difopab  4973  rexiunxp  4982  rexxpf  4987  somin1  5237  cnvdif  5245  imadif  5495  brprcneu  5688  dffv2  5763  difxp  6347  poxp  6425  porpss  6493  tz7.48lem  6665  brsdom  7097  brsdom2  7198  fimax2g  7320  ordunifi  7324  dfsup2  7413  dfsup2OLD  7414  suc11reg  7538  rankxplim2  7768  rankxplim3  7769  alephval3  7955  kmlem4  7997  cflim2  8107  isfin4-2  8158  fin23lem25  8168  fin1a2lem5  8248  fin12  8257  axcclem  8301  zorng  8348  infinf  8405  alephadd  8416  fpwwe2  8482  axpre-lttri  9004  dfinfmr  9949  infmsup  9950  infmrgelb  9952  infmrlb  9953  arch  10182  rpneg  10605  xmulcom  10809  xmulneg1  10812  xmulf  10815  xrinfmss2  10853  difreicc  10992  hashfun  11663  incexc2  12581  fctop  17031  cctop  17033  ntreq0  17104  ordtbas2  17217  cmpcld  17427  hausdiag  17638  fbun  17833  fbfinnfr  17834  opnfbas  17835  fbasrn  17877  filuni  17878  ufinffr  17922  alexsubALTlem2  18040  ellogdm  20491  usgraidx2v  21373  avril1  21718  shne0i  22911  chnlei  22948  cvnbtwn2  23751  cvnbtwn3  23752  cvnbtwn4  23753  chrelat2i  23829  atabs2i  23866  dmdbr5ati  23886  nmo  23934  disjdifprg  23978  eliccelico  24101  elicoelioo  24102  xrdifh  24104  tosglb  24153  xrnarchi  24215  hasheuni  24436  cntnevol  24543  sibfof  24615  ballotlem2  24707  ballotlemodife  24716  erdszelem9  24846  fzp1nel  25171  dftr6  25329  fundmpss  25344  dfon2lem5  25365  dfon2lem8  25368  dfon2lem9  25369  nodenselem7  25563  nocvxminlem  25566  symdifass  25593  dffun10  25675  elfuns  25676  tfrqfree  25712  df3nandALT1  26058  andnand1  26060  imnand2  26061  gtinf  26220  fdc  26347  nninfnub  26353  n0el  26606  ctbnfien  26777  rencldnfilem  26779  numinfctb  27144  f1omvdco3  27268  psgnunilem4  27296  gsumcom3  27330  compab  27519  otiunsndisj  27962  otiunsndisjX  27963  2spotiundisj  28173  zfregs2VD  28671  undif3VD  28712  onfrALTlem5VD  28715  bnj1143  28879  bnj1304  28909  bnj1476  28936  bnj1533  28941  bnj1174  29090  bnj1204  29099  bnj1280  29107  cbvexwAUX7  29236  sb8ewAUX7  29307  cbvexOLD7  29422  sbcomOLD7  29451  sb8eOLD7  29453  lcvnbtwn2  29522  lcvnbtwn3  29523  cvrnbtwn3  29771  dalem18  30175  lhpocnel2  30513  cdleme0nex  30784  cdlemk19w  31466  dihglblem6  31835  dvh2dim  31940  dvh3dim3N  31944
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