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  2729  cbvrexcsf  3105  dfss4  3364  indifdir  3386  difprsn  3716  brdif  4031  pwundifOLD  4259  tfinds  4608  difopab  4791  rexiunxp  4800  rexxpf  4805  somin1  5053  cnvdif  5061  imadif  5251  dffv2  5512  difxp  6073  poxp  6147  porpss  6201  tz7.48lem  6407  brsdom  6838  brsdom2  6939  fimax2g  7057  ordunifi  7061  dfsup2  7149  dfsup2OLD  7150  suc11reg  7274  rankxplim2  7504  rankxplim3  7505  alephval3  7691  kmlem4  7733  cflim2  7843  isfin4-2  7894  fin23lem25  7904  fin1a2lem5  7984  fin12  7993  axcclem  8037  zorng  8085  infinf  8142  alephadd  8153  fpwwe2  8219  axpre-lttri  8741  dfinfmr  9685  infmsup  9686  infmrgelb  9688  infmrlb  9689  arch  9915  rpneg  10336  xmulcom  10538  xmulneg1  10541  xmulf  10544  xrinfmss2  10581  difreicc  10719  hashfun  11340  fctop  16689  cctop  16691  ntreq0  16762  ordtbas2  16869  cmpcld  17077  hausdiag  17287  fbun  17483  fbfinnfr  17484  opnfbas  17485  fbasrn  17527  filuni  17528  ufinffr  17572  alexsubALTlem2  17690  ellogdm  19934  avril1  20782  shne0i  21973  chnlei  22010  cvnbtwn2  22813  cvnbtwn3  22814  cvnbtwn4  22815  chrelat2i  22891  atabs2i  22928  dmdbr5ati  22948  ballotlem2  22994  ballotlemodife  23003  ballotlem4  23004  ballotlemimin  23011  erdszelem9  23088  dftr6  23464  fundmpss  23477  dfon2lem5  23498  dfon2lem8  23501  dfon2lem9  23502  axdenselem7  23696  nocvxminlem  23699  axfelem22  23722  symdifass  23733  tfrqfree  23850  df3nandALT1  24196  andnand1  24198  imnand2  24199  albineal  24351  evevifev  24366  gtinf  25587  fdc  25808  nninfnub  25814  n0el  26078  ctbnfien  26254  rencldnfilem  26256  numinfctb  26621  f1omvdco3  26745  psgnunilem4  26773  gsumcom3  26807  compab  26998  fmul01lt1lem2  27069  zfregs2VD  27651  undif3VD  27692  onfrALTlem5VD  27695  bnj1143  27855  bnj1304  27885  bnj1476  27912  bnj1533  27917  bnj1174  28066  bnj1204  28075  bnj1280  28083  cbvexvK  28164  ax12o10lem5K  28189  ax12-4  28257  lcvnbtwn2  28368  lcvnbtwn3  28369  cvrnbtwn3  28617  dalem18  29021  lhpocnel2  29359  cdleme0nex  29630  cdlemk19w  30312  dihglblem6  30681  dvh2dim  30786  dvh3dim3N  30790
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