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  1799  cbvexvw  1956  hbn1fw  1958  hba1w  1960  excom  2028  cbvexv1  2163  cbvex  2259  cbvexv  2262  cbvex2  2267  cbvrexf  3141  cbvrexcsf  3531  elsymdifxor  3811  symdifass  3814  dfss4  3819  indifdir  3841  neq0f  3884  ab0  3904  pssdifcom2  4006  difprsnss  4269  brdif  4629  otiunsndisj  4896  difopab  5163  rexiunxp  5172  rexxpf  5179  somin1  5435  cnvdif  5444  difxp  5463  imadif  5873  brprcneu  6081  dffv2  6166  ovima0  6688  porpss  6816  tfinds  6928  poxp  7153  tz7.48lem  7400  brsdom  7841  brsdom2  7946  fimax2g  8068  ordunifi  8072  dfsup2  8210  supgtoreq  8236  infcllem  8253  suc11reg  8376  rankxplim2  8603  rankxplim3  8604  alephval3  8793  kmlem4  8835  cflim2  8945  isfin4-2  8996  fin23lem25  9006  fin1a2lem5  9086  fin12  9095  axcclem  9139  zorng  9186  infinf  9244  alephadd  9255  fpwwe2  9321  axpre-lttri  9842  dfinfre  10851  infrenegsup  10853  arch  11136  rpneg  11695  xmulcom  11925  xmulneg1  11928  xmulf  11931  xrinfmss2  11969  difreicc  12131  fzp1nel  12248  ssnn0fi  12601  fsuppmapnn0fiubex  12609  hashfun  13036  swrdccatin2  13284  s3iunsndisj  13501  incexc2  14355  lcmftp  15133  f1omvdco3  17638  psgnunilem4  17686  0ringnnzr  19036  gsumcom3  19966  mdetunilem7  20185  fctop  20560  cctop  20562  ntreq0  20633  ordtbas2  20747  cmpcld  20957  hausdiag  21200  fbun  21396  fbfinnfr  21397  opnfbas  21398  fbasrn  21440  filuni  21441  ufinffr  21485  alexsubALTlem2  21604  ellogdm  24102  usgraidx2v  25688  2spotiundisj  26355  avril1  26477  shne0i  27497  chnlei  27534  cvnbtwn2  28336  cvnbtwn3  28337  cvnbtwn4  28338  chrelat2i  28414  atabs2i  28451  dmdbr5ati  28471  nmo  28515  disjdifprg  28576  eliccelico  28735  elicoelioo  28736  xrdifh  28738  f1ocnt  28752  tosglblem  28806  xrnarchi  28875  hasheuni  29280  cntnevol  29424  sitgaddlemb  29543  eulerpartlemgs2  29575  ballotlem2  29683  ballotlemodife  29692  plymulx0  29756  bnj1143  29921  bnj1304  29950  bnj1476  29977  bnj1533  29982  bnj1174  30131  bnj1204  30140  bnj1280  30148  erdszelem9  30241  dftr6  30699  fundmpss  30716  dfon2lem5  30742  dfon2lem8  30745  dfon2lem9  30746  wzel  30821  wzelOLD  30822  nosepon  30872  nodenselem7  30892  nocvxminlem  30895  elfuns  30998  dfrecs2  31033  gtinfOLD  31290  df3nandALT1  31372  andnand1  31374  imnand2  31375  bj-notalbii  31589  bj-cbvex2v  31731  fdc  32507  nninfnub  32513  tsbi4  32909  ts3an2  32924  ts3an3  32925  ts3or1  32926  n0el  32960  lcvnbtwn2  33128  lcvnbtwn3  33129  cvrnbtwn3  33377  dalem18  33781  lhpocnel2  34119  cdleme0nex  34391  cdlemk19w  35074  dihglblem6  35443  dvh2dim  35548  dvh3dim3N  35552  ctbnfien  36196  rencldnfilem  36198  numinfctb  36488  ifpnorcor  36640  ifpnancor  36641  ifpdfnan  36646  ifpananb  36666  ifpnannanb  36667  ifpxorxorb  36671  rp-fakenanass  36675  rp-isfinite6  36679  pwinfig  36681  elnonrel  36706  iunrelexp0  36809  frege131  37104  frege133  37106  compab  37462  zfregs2VD  37894  undif3VD  37936  onfrALTlem5VD  37939  sineq0ALT  37991  ndisj2  38039  disjrnmpt2  38166  icccncfext  38570  itgioocnicc  38666  fourierdlem42  38839  fourierdlem62  38858  fourierdlem93  38889  fourierdlem101  38897  nsssmfmbf  39462  nltle2tri  39740  evennodd  39892  otiunsndisjX  40125  usgredg2v  40449  2wspiundisj  41161
  Copyright terms: Public domain W3C validator