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

Theorem notbii 308
Description: Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
notbii.1 (𝜑𝜓)
Assertion
Ref Expression
notbii 𝜑 ↔ ¬ 𝜓)

Proof of Theorem notbii
StepHypRef Expression
1 notbii.1 . 2 (𝜑𝜓)
2 notbi 307 . 2 ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
31, 2mpbi 218 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  sylnbi  318  xchnxbi  320  xchbinx  322  oplem1  998  xorcom  1458  xorbi12i  1468  nic-axALT  1589  tbw-bijust  1613  rb-bijust  1664  19.43OLD  1781  cbvexvw  1919  hbn1fw  1921  excom  1978  cbvexv1  2116  cbvex  2163  cbvexv  2166  cbvex2  2171  cbvrexf  3046  cbvrexcsf  3436  elsymdifxor  3715  symdifass  3718  dfss4  3723  indifdir  3745  neq0f  3788  ab0  3808  pssdifcom2  3910  difprsnss  4173  brdif  4533  otiunsndisj  4800  difopab  5067  rexiunxp  5076  rexxpf  5083  somin1  5339  cnvdif  5348  difxp  5367  imadif  5777  brprcneu  5985  dffv2  6070  ovima0  6592  porpss  6720  tfinds  6832  poxp  7056  tz7.48lem  7303  brsdom  7744  brsdom2  7849  fimax2g  7971  ordunifi  7975  dfsup2  8113  supgtoreq  8139  infcllem  8156  suc11reg  8279  rankxplim2  8506  rankxplim3  8507  alephval3  8696  kmlem4  8738  cflim2  8848  isfin4-2  8899  fin23lem25  8909  fin1a2lem5  8989  fin12  8998  axcclem  9042  zorng  9089  infinf  9147  alephadd  9158  fpwwe2  9224  axpre-lttri  9745  dfinfre  10759  infrenegsup  10761  infmsupOLD  10762  infmrgelbOLD  10765  infmrlbOLD  10767  arch  11048  rpneg  11609  xmulcom  11839  xmulneg1  11842  xmulf  11845  xrinfmss2  11883  difreicc  12048  fzp1nel  12165  ssnn0fi  12518  fsuppmapnn0fiubex  12526  hashfun  12953  swrdccatin2  13201  s3iunsndisj  13418  incexc2  14282  lcmftp  15067  f1omvdco3  17588  psgnunilem4  17636  0ringnnzr  18998  gsumcom3  19931  mdetunilem7  20150  fctop  20525  cctop  20527  ntreq0  20598  ordtbas2  20712  cmpcld  20922  hausdiag  21165  fbun  21361  fbfinnfr  21362  opnfbas  21363  fbasrn  21405  filuni  21406  ufinffr  21450  alexsubALTlem2  21569  ellogdm  24076  usgraidx2v  25664  2spotiundisj  26331  avril1  26453  shne0i  27483  chnlei  27520  cvnbtwn2  28322  cvnbtwn3  28323  cvnbtwn4  28324  chrelat2i  28400  atabs2i  28437  dmdbr5ati  28457  nmo  28501  disjdifprg  28562  eliccelico  28728  elicoelioo  28729  xrdifh  28731  f1ocnt  28745  tosglblem  28799  xrnarchi  28869  hasheuni  29274  cntnevol  29418  omssubaddOLD  29499  sitgaddlemb  29548  eulerpartlemgs2  29580  ballotlem2  29688  ballotlemodife  29697  plymulx0  29799  bnj1143  29964  bnj1304  29993  bnj1476  30020  bnj1533  30025  bnj1174  30174  bnj1204  30183  bnj1280  30191  erdszelem9  30284  dftr6  30739  fundmpss  30756  dfon2lem5  30782  dfon2lem8  30785  dfon2lem9  30786  wzel  30856  nosepon  30905  nodenselem7  30925  nocvxminlem  30928  elfuns  31031  dfrecs2  31066  gtinf  31322  df3nandALT1  31404  andnand1  31406  imnand2  31407  bj-notalbii  31621  bj-cbvex2v  31763  fdc  32605  nninfnub  32611  tsbi4  33007  ts3an2  33022  ts3an3  33023  ts3or1  33024  n0el  33058  lcvnbtwn2  33226  lcvnbtwn3  33227  cvrnbtwn3  33475  dalem18  33879  lhpocnel2  34217  cdleme0nex  34489  cdlemk19w  35172  dihglblem6  35541  dvh2dim  35646  dvh3dim3N  35650  ctbnfien  36294  rencldnfilem  36296  numinfctb  36586  ifpnorcor  36745  ifpnancor  36746  ifpdfnan  36751  ifpananb  36771  ifpnannanb  36772  ifpxorxorb  36776  rp-fakenanass  36780  rp-isfinite6  36784  pwinfig  36786  elnonrel  36811  iunrelexp0  36914  frege131  37209  frege133  37211  compab  37567  zfregs2VD  37999  undif3VD  38041  onfrALTlem5VD  38044  sineq0ALT  38096  ndisj2  38145  disjrnmpt2  38272  icccncfext  38677  itgioocnicc  38776  fourierdlem42  38950  fourierdlem42OLD  38951  fourierdlem62  38970  fourierdlem93  39001  fourierdlem101  39009  nsssmfmbf  39576  nltle2tri  39854  evennodd  40006  otiunsndisjX  40239  usgredg2v  40563  2wspiundisj  41275
  Copyright terms: Public domain W3C validator