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  2713  cbvrexcsf  3086  dfss4  3345  indifdir  3367  difprsn  3697  brdif  4011  pwundifOLD  4238  tfinds  4587  difopab  4770  rexiunxp  4779  rexxpf  4784  somin1  5032  cnvdif  5040  imadif  5230  dffv2  5491  difxp  6052  poxp  6126  porpss  6180  tz7.48lem  6386  brsdom  6817  brsdom2  6918  fimax2g  7036  ordunifi  7040  dfsup2  7128  dfsup2OLD  7129  suc11reg  7253  rankxplim2  7483  rankxplim3  7484  alephval3  7670  kmlem4  7712  cflim2  7822  isfin4-2  7873  fin23lem25  7883  fin1a2lem5  7963  fin12  7972  axcclem  8016  zorng  8064  infinf  8121  alephadd  8132  fpwwe2  8198  axpre-lttri  8720  dfinfmr  9664  infmsup  9665  infmrgelb  9667  infmrlb  9668  arch  9894  rpneg  10315  xmulcom  10517  xmulneg1  10520  xmulf  10523  xrinfmss2  10560  difreicc  10698  hashfun  11319  fctop  16668  cctop  16670  ntreq0  16741  ordtbas2  16848  cmpcld  17056  hausdiag  17266  fbun  17462  fbfinnfr  17463  opnfbas  17464  fbasrn  17506  filuni  17507  ufinffr  17551  alexsubALTlem2  17669  ellogdm  19913  avril1  20761  shne0i  21952  chnlei  21989  cvnbtwn2  22792  cvnbtwn3  22793  cvnbtwn4  22794  chrelat2i  22870  atabs2i  22907  dmdbr5ati  22927  ballotlem2  22973  ballotlemodife  22982  ballotlem4  22983  ballotlemimin  22990  erdszelem9  23067  dftr6  23443  fundmpss  23456  dfon2lem5  23477  dfon2lem8  23480  dfon2lem9  23481  axdenselem7  23675  nocvxminlem  23678  axfelem22  23701  symdifass  23712  tfrqfree  23829  df3nandALT1  24175  andnand1  24177  imnand2  24178  albineal  24330  evevifev  24345  gtinf  25566  fdc  25787  nninfnub  25793  n0el  26057  ctbnfien  26233  rencldnfilem  26235  numinfctb  26600  f1omvdco3  26724  psgnunilem4  26752  gsumcom3  26786  compab  26977  fmul01lt1lem2  27048  zfregs2VD  27630  undif3VD  27671  onfrALTlem5VD  27674  bnj1143  27834  bnj1304  27864  bnj1476  27891  bnj1533  27896  bnj1174  28045  bnj1204  28054  bnj1280  28062  cbvexvK  28143  ax12o10lem5K  28168  ax12-4  28236  lcvnbtwn2  28347  lcvnbtwn3  28348  cvrnbtwn3  28596  dalem18  29000  lhpocnel2  29338  cdleme0nex  29609  cdlemk19w  30291  dihglblem6  30660  dvh2dim  30765  dvh3dim3N  30769
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