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

Theorem notbii 305
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 304 . 2 ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
31, 2mpbi 215 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 191
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 192
This theorem is referenced by:  sylnbi  315  xchnxbi  317  xchbinx  319  oplem1  989  xorcom  1449  xorassOLD  1451  xorneg2OLD  1460  xorbi12i  1462  trunanfalOLD  1512  falxortruOLD  1518  nic-axALT  1587  tbw-bijust  1611  rb-bijust  1662  19.43OLD  1777  cbvexvw  1918  hbn1fw  1920  excom  1977  excomOLD  1978  cbvexv1  2117  cbvex  2162  cbvex2  2168  cbvrexf  3035  cbvrexcsf  3418  elsymdifxor  3696  symdifass  3699  dfss4  3704  indifdir  3726  difprsnss  4136  brdif  4485  otiunsndisj  4748  difopab  5013  rexiunxp  5022  rexxpf  5029  somin1  5283  cnvdif  5292  difxp  5311  imadif  5713  brprcneu  5920  dffv2  6005  ovima0  6523  porpss  6651  tfinds  6763  poxp  6987  tz7.48lem  7235  brsdom  7675  brsdom2  7780  fimax2g  7902  ordunifi  7906  dfsup2  8043  supgtoreq  8069  infcllem  8086  suc11reg  8209  rankxplim2  8436  rankxplim3  8437  alephval3  8626  kmlem4  8668  cflim2  8778  isfin4-2  8829  fin23lem25  8839  fin1a2lem5  8919  fin12  8928  axcclem  8972  zorng  9019  infinf  9076  alephadd  9087  fpwwe2  9153  axpre-lttri  9674  dfinfre  10677  dfinfmrOLD  10678  infrenegsup  10680  infmsupOLD  10681  infmrgelbOLD  10684  infmrlbOLD  10686  arch  10957  rpneg  11423  xmulcom  11647  xmulneg1  11650  xmulf  11653  xrinfmss2  11691  difreicc  11860  fzp1nel  11976  ssnn0fi  12311  fsuppmapnn0fiubex  12318  hashfun  12729  swrdccatin2  12976  s3iunsndisj  13193  incexc2  14056  lcmftp  14771  f1omvdco3  17251  psgnunilem4  17299  0ringnnzr  18652  gsumcom3  19582  mdetunilem7  19801  fctop  20176  cctop  20178  ntreq0  20250  ordtbas2  20364  cmpcld  20574  hausdiag  20817  fbun  21013  fbfinnfr  21014  opnfbas  21015  fbasrn  21057  filuni  21058  ufinffr  21102  alexsubALTlem2  21221  ellogdm  23745  usgraidx2v  25281  2spotiundisj  25950  avril1  26061  shne0i  27264  chnlei  27301  cvnbtwn2  28103  cvnbtwn3  28104  cvnbtwn4  28105  chrelat2i  28181  atabs2i  28218  dmdbr5ati  28238  nmo  28282  disjdifprg  28344  eliccelico  28515  elicoelioo  28516  xrdifh  28518  f1ocnt  28532  tosglblem  28586  xrnarchi  28656  hasheuni  29061  cntnevol  29205  omssubaddOLD  29286  sitgaddlemb  29335  eulerpartlemgs2  29367  ballotlem2  29475  ballotlemodife  29484  plymulx0  29589  bnj1143  29754  bnj1304  29783  bnj1476  29810  bnj1533  29815  bnj1174  29964  bnj1204  29973  bnj1280  29981  erdszelem9  30074  dftr6  30541  fundmpss  30558  dfon2lem5  30584  dfon2lem8  30587  dfon2lem9  30588  wzel  30658  nosepon  30707  nodenselem7  30727  nocvxminlem  30730  elfuns  30833  dfrecs2  30868  gtinf  31124  df3nandALT1  31206  andnand1  31208  imnand2  31209  bj-cbvex2v  31526  fdc  32311  nninfnub  32317  tsbi4  32614  ts3an2  32629  ts3an3  32630  ts3or1  32631  n0el  32666  lcvnbtwn2  32833  lcvnbtwn3  32834  cvrnbtwn3  33082  dalem18  33486  lhpocnel2  33824  cdleme0nex  34096  cdlemk19w  34779  dihglblem6  35148  dvh2dim  35253  dvh3dim3N  35257  ctbnfien  35901  rencldnfilem  35903  numinfctb  36202  ifpnorcor  36364  ifpnancor  36365  ifpdfnan  36370  ifpananb  36390  ifpnannanb  36391  ifpxorxorb  36395  rp-fakenanass  36399  rp-isfinite6  36403  pwinfig  36405  elnonrel  36430  iunrelexp0  36533  frege131  36829  frege133  36831  compab  37151  zfregs2VD  37585  undif3VD  37627  onfrALTlem5VD  37630  sineq0ALT  37682  ndisj2  37732  disjrnmpt2  37823  icccncfext  38174  itgioocnicc  38273  fourierdlem42  38448  fourierdlem42OLD  38449  fourierdlem62  38468  fourierdlem93  38499  fourierdlem101  38507  nltle2tri  39236  evennodd  39293  otiunsndisjX  39527  usgredg2v  39854  2wspiundisj  40566
  Copyright terms: Public domain W3C validator