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

Theorem notbii 287
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 286 . 2  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
31, 2mpbi 199 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  sylnbi  297  xchnxbi  299  xchbinx  301  oplem1  930  nancom  1290  xorcom  1298  xorass  1299  xorneg2  1303  xorbi12i  1305  trunanfal  1345  falxortru  1350  hadnot  1383  cadnot  1384  nic-axALT  1429  tbw-bijust  1453  rb-bijust  1504  19.43OLD  1593  cbvexvw  1678  cbvex  1928  sb8e  2032  cbvrexf  2760  cbvrexcsf  3145  dfss4  3404  indifdir  3426  difprsn  3757  brdif  4072  pwundifOLD  4300  tfinds  4649  difopab  4816  rexiunxp  4825  rexxpf  4830  somin1  5078  cnvdif  5086  imadif  5293  dffv2  5554  difxp  6115  poxp  6189  porpss  6243  tz7.48lem  6449  brsdom  6880  brsdom2  6981  fimax2g  7099  ordunifi  7103  dfsup2  7191  dfsup2OLD  7192  suc11reg  7316  rankxplim2  7546  rankxplim3  7547  alephval3  7733  kmlem4  7775  cflim2  7885  isfin4-2  7936  fin23lem25  7946  fin1a2lem5  8026  fin12  8035  axcclem  8079  zorng  8127  infinf  8184  alephadd  8195  fpwwe2  8261  axpre-lttri  8783  dfinfmr  9727  infmsup  9728  infmrgelb  9730  infmrlb  9731  arch  9958  rpneg  10379  xmulcom  10582  xmulneg1  10585  xmulf  10588  xrinfmss2  10625  difreicc  10763  hashfun  11385  incexc2  12293  fctop  16737  cctop  16739  ntreq0  16810  ordtbas2  16917  cmpcld  17125  hausdiag  17335  fbun  17531  fbfinnfr  17532  opnfbas  17533  fbasrn  17575  filuni  17576  ufinffr  17620  alexsubALTlem2  17738  ellogdm  19982  avril1  20830  shne0i  22023  chnlei  22060  cvnbtwn2  22863  cvnbtwn3  22864  cvnbtwn4  22865  chrelat2i  22941  atabs2i  22978  dmdbr5ati  22998  ballotlem2  23043  ballotlemodife  23052  ballotlem4  23053  ballotlemimin  23060  erdszelem9  23137  dftr6  23513  fundmpss  23526  dfon2lem5  23547  dfon2lem8  23550  dfon2lem9  23551  axdenselem7  23745  nocvxminlem  23748  axfelem22  23771  symdifass  23782  tfrqfree  23899  df3nandALT1  24245  andnand1  24247  imnand2  24248  albineal  24409  evevifev  24424  gtinf  25645  fdc  25866  nninfnub  25872  n0el  26136  ctbnfien  26312  rencldnfilem  26314  numinfctb  26679  f1omvdco3  26803  psgnunilem4  26831  gsumcom3  26865  compab  27055  fmul01lt1lem2  27126  zfregs2VD  27897  undif3VD  27938  onfrALTlem5VD  27941  bnj1143  28101  bnj1304  28131  bnj1476  28158  bnj1533  28163  bnj1174  28312  bnj1204  28321  bnj1280  28329  ax12-4  28385  lcvnbtwn2  28496  lcvnbtwn3  28497  cvrnbtwn3  28745  dalem18  29149  lhpocnel2  29487  cdleme0nex  29758  cdlemk19w  30440  dihglblem6  30809  dvh2dim  30914  dvh3dim3N  30918
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 177
  Copyright terms: Public domain W3C validator