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

Theorem notbii 322
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 321 . 2 ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
31, 2mpbi 232 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208
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 209
This theorem is referenced by:  sylnbi  332  xchnxbi  334  xchbinx  336  oplem1  1050  xorcom  1500  xorbi12i  1510  norcom  1516  noranOLD  1520  nororOLD  1522  norassOLD  1527  nic-axALT  1668  tbw-bijust  1692  rb-bijust  1743  19.43OLD  1877  cbvexvw  2037  hbn1fw  2045  hba1w  2047  excom  2161  sbnvOLD  2315  cbvexv1  2355  cbvex2v  2358  cbvrexfw  3437  cbvrexf  3439  cbvrexcsf  3924  dfss4  4233  indifdir  4258  neq0f  4304  n0el  4319  ab0  4331  pssdifcom2  4434  difprsnss  4724  brdif  5110  otiunsndisj  5401  difopab  5695  rexiunxp  5704  rexxpf  5711  rnep  5790  somin1  5986  cnvdif  5995  difxp  6014  imadif  6431  brprcneu  6655  dffv2  6749  ovima0  7319  porpss  7445  tfinds  7566  poxp  7814  tz7.48lem  8069  brsdom  8524  brsdom2  8633  fimax2g  8756  ordunifi  8760  dfsup2  8900  supgtoreq  8926  infcllem  8943  suc11reg  9074  rankxplim2  9301  rankxplim3  9302  alephval3  9528  kmlem4  9571  cflim2  9677  isfin4-2  9728  fin23lem25  9738  fin1a2lem5  9818  fin12  9827  axcclem  9871  zorng  9918  infinf  9980  alephadd  9991  fpwwe2  10057  axpre-lttri  10579  dfinfre  11614  infrenegsup  11616  arch  11886  rpneg  12413  xmulcom  12651  xmulneg1  12654  xmulf  12657  xrinfmss2  12696  difreicc  12862  fzp1nel  12983  ssnn0fi  13345  fsuppmapnn0fiubex  13352  hashfun  13790  swrdccatin2  14083  s3iunsndisj  14320  incexc2  15185  lcmftp  15972  f1omvdco3  18569  psgnunilem4  18617  gsumcom3  19090  gsumxp2  19092  0ringnnzr  20034  mdetunilem7  21219  fctop  21604  cctop  21606  ntreq0  21677  ordtbas2  21791  cmpcld  22002  hausdiag  22245  fbun  22440  fbfinnfr  22441  opnfbas  22442  fbasrn  22484  filuni  22485  ufinffr  22529  alexsubALTlem2  22648  ellogdm  25214  numedglnl  26921  usgredg2v  27001  clwwlknon1nloop  27870  avril1  28234  shne0i  29217  chnlei  29254  cvnbtwn2  30056  cvnbtwn3  30057  cvnbtwn4  30058  chrelat2i  30134  atabs2i  30171  dmdbr5ati  30191  nelbOLD  30224  nmo  30246  disjdifprg  30317  eliccelico  30492  elicoelioo  30493  xrdifh  30495  f1ocnt  30517  tosglblem  30649  xrnarchi  30806  hasheuni  31332  cntnevol  31475  sitgaddlemb  31594  eulerpartlemgs2  31626  ballotlem2  31734  ballotlemodife  31743  plymulx0  31805  bnj1143  32050  bnj1304  32079  bnj1476  32107  bnj1533  32112  bnj1174  32263  bnj1204  32272  bnj1280  32280  0nn0m1nnn0  32339  lfuhgr3  32354  erdszelem9  32434  fmla0disjsuc  32633  dftr6  32974  fundmpss  32997  dfon2lem5  33020  dfon2lem8  33023  dfon2lem9  33024  wzel  33099  nosepon  33160  noextenddif  33163  nomaxmo  33189  nocvxminlem  33235  elfuns  33364  dfrecs2  33399  df3nandALT1  33735  andnand1  33737  imnand2  33738  bj-notalbii  33936  difunieq  34642  domalom  34672  fvineqsneq  34680  wl-dfrexv  34836  wl-dfrexex  34837  fdc  35007  nninfnub  35013  tsbi4  35401  ts3an2  35416  ts3an3  35417  ts3or1  35418  vvdifopab  35508  brvvdif  35511  n0elqs  35570  dfssr2  35726  lcvnbtwn2  36150  lcvnbtwn3  36151  cvrnbtwn3  36399  dalem18  36804  lhpocnel2  37142  cdleme0nex  37413  cdlemk19w  38095  dihglblem6  38463  dvh2dim  38568  dvh3dim3N  38572  ctbnfien  39400  rencldnfilem  39402  numinfctb  39688  ifpnorcor  39831  ifpnancor  39832  ifpdfnan  39837  ifpananb  39857  ifpnannanb  39858  ifpxorxorb  39862  rp-isfinite6  39869  pwinfig  39905  elnonrel  39930  iunrelexp0  40032  frege131  40325  frege133  40327  compab  40759  zfregs2VD  41160  undif3VD  41201  sineq0ALT  41256  ndisj2  41298  uz0  41670  icccncfext  42154  itgioocnicc  42246  fourierdlem42  42419  fourierdlem62  42438  fourierdlem93  42469  fourierdlem101  42477  nsssmfmbf  43040  aiotavb  43275  afv2ndeffv0  43444  otiunsndisjX  43463  nltle2tri  43498  0nelsetpreimafv  43535  evennodd  43793  setrec2lem1  44781
  Copyright terms: Public domain W3C validator