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

Theorem notbii 309
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 308 . 2 ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
31, 2mpbi 219 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 195
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 196
This theorem is referenced by:  sylnbi  319  xchnxbi  321  xchbinx  323  oplem1  999  xorcom  1459  xorbi12i  1469  nic-axALT  1590  tbw-bijust  1614  rb-bijust  1665  19.43OLD  1800  cbvexvw  1957  hbn1fw  1959  hba1w  1961  excom  2029  cbvexv1  2164  cbvex  2260  cbvexv  2263  cbvex2  2268  cbvrexf  3142  cbvrexcsf  3532  elsymdifxor  3812  symdifass  3815  dfss4  3820  indifdir  3842  neq0f  3885  ab0  3905  pssdifcom2  4007  difprsnss  4270  brdif  4635  otiunsndisj  4905  difopab  5175  rexiunxp  5184  rexxpf  5191  somin1  5448  cnvdif  5458  difxp  5477  imadif  5887  brprcneu  6096  dffv2  6181  ovima0  6711  porpss  6839  tfinds  6951  poxp  7176  tz7.48lem  7423  brsdom  7864  brsdom2  7969  fimax2g  8091  ordunifi  8095  dfsup2  8233  supgtoreq  8259  infcllem  8276  suc11reg  8399  rankxplim2  8626  rankxplim3  8627  alephval3  8816  kmlem4  8858  cflim2  8968  isfin4-2  9019  fin23lem25  9029  fin1a2lem5  9109  fin12  9118  axcclem  9162  zorng  9209  infinf  9267  alephadd  9278  fpwwe2  9344  axpre-lttri  9865  dfinfre  10881  infrenegsup  10883  arch  11166  rpneg  11739  xmulcom  11968  xmulneg1  11971  xmulf  11974  xrinfmss2  12013  difreicc  12175  fzp1nel  12293  ssnn0fi  12646  fsuppmapnn0fiubex  12654  hashfun  13084  swrdccatin2  13338  s3iunsndisj  13555  incexc2  14409  lcmftp  15187  f1omvdco3  17692  psgnunilem4  17740  0ringnnzr  19090  gsumcom3  20024  mdetunilem7  20243  fctop  20618  cctop  20620  ntreq0  20691  ordtbas2  20805  cmpcld  21015  hausdiag  21258  fbun  21454  fbfinnfr  21455  opnfbas  21456  fbasrn  21498  filuni  21499  ufinffr  21543  alexsubALTlem2  21662  ellogdm  24185  usgraidx2v  25922  2spotiundisj  26589  avril1  26711  shne0i  27691  chnlei  27728  cvnbtwn2  28530  cvnbtwn3  28531  cvnbtwn4  28532  chrelat2i  28608  atabs2i  28645  dmdbr5ati  28665  nmo  28709  disjdifprg  28770  eliccelico  28929  elicoelioo  28930  xrdifh  28932  f1ocnt  28946  tosglblem  29000  xrnarchi  29069  hasheuni  29474  cntnevol  29618  sitgaddlemb  29737  eulerpartlemgs2  29769  ballotlem2  29877  ballotlemodife  29886  plymulx0  29950  bnj1143  30115  bnj1304  30144  bnj1476  30171  bnj1533  30176  bnj1174  30325  bnj1204  30334  bnj1280  30342  erdszelem9  30435  dftr6  30893  fundmpss  30910  dfon2lem5  30936  dfon2lem8  30939  dfon2lem9  30940  wzel  31015  wzelOLD  31016  nosepon  31066  nodenselem7  31086  nocvxminlem  31089  elfuns  31192  dfrecs2  31227  gtinfOLD  31484  df3nandALT1  31566  andnand1  31568  imnand2  31569  bj-notalbii  31783  bj-cbvex2v  31925  fdc  32711  nninfnub  32717  tsbi4  33113  ts3an2  33128  ts3an3  33129  ts3or1  33130  n0el  33164  lcvnbtwn2  33332  lcvnbtwn3  33333  cvrnbtwn3  33581  dalem18  33985  lhpocnel2  34323  cdleme0nex  34595  cdlemk19w  35278  dihglblem6  35647  dvh2dim  35752  dvh3dim3N  35756  ctbnfien  36400  rencldnfilem  36402  numinfctb  36692  ifpnorcor  36844  ifpnancor  36845  ifpdfnan  36850  ifpananb  36870  ifpnannanb  36871  ifpxorxorb  36875  rp-fakenanass  36879  rp-isfinite6  36883  pwinfig  36885  elnonrel  36910  iunrelexp0  37013  frege131  37308  frege133  37310  compab  37666  zfregs2VD  38098  undif3VD  38140  onfrALTlem5VD  38143  sineq0ALT  38195  ndisj2  38243  disjrnmpt2  38370  icccncfext  38773  itgioocnicc  38869  fourierdlem42  39042  fourierdlem62  39061  fourierdlem93  39092  fourierdlem101  39100  nsssmfmbf  39665  nltle2tri  39942  evennodd  40094  otiunsndisjX  40317  usgredg2v  40454  2wspiundisj  41166  setrec2lem1  42239
  Copyright terms: Public domain W3C validator