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

Theorem notbii 310
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 309 . 2 ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
31, 2mpbi 220 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  sylnbi  320  xchnxbi  322  xchbinx  324  oplem1  1006  xorcom  1464  xorbi12i  1474  nic-axALT  1596  tbw-bijust  1620  rb-bijust  1671  19.43OLD  1811  cbvexvw  1972  hbn1fw  1974  hba1w  1976  excom  2044  cbvexv1  2180  cbvex  2276  cbvexv  2279  cbvex2  2284  cbvrexf  3159  cbvrexcsf  3552  elsymdifxor  3833  symdifass  3836  dfss4  3841  indifdir  3864  neq0f  3907  ab0  3930  pssdifcom2  4032  difprsnss  4303  brdif  4670  otiunsndisj  4945  difopab  5218  rexiunxp  5227  rexxpf  5234  somin1  5492  cnvdif  5502  difxp  5521  imadif  5933  brprcneu  6143  dffv2  6229  ovima0  6767  porpss  6895  tfinds  7007  poxp  7235  tz7.48lem  7482  brsdom  7923  brsdom2  8029  fimax2g  8151  ordunifi  8155  dfsup2  8295  supgtoreq  8321  infcllem  8338  suc11reg  8461  rankxplim2  8688  rankxplim3  8689  alephval3  8878  kmlem4  8920  cflim2  9030  isfin4-2  9081  fin23lem25  9091  fin1a2lem5  9171  fin12  9180  axcclem  9224  zorng  9271  infinf  9333  alephadd  9344  fpwwe2  9410  axpre-lttri  9931  dfinfre  10949  infrenegsup  10951  arch  11234  rpneg  11807  xmulcom  12036  xmulneg1  12039  xmulf  12042  xrinfmss2  12081  difreicc  12243  fzp1nel  12362  ssnn0fi  12721  fsuppmapnn0fiubex  12729  hashfun  13161  swrdccatin2  13419  s3iunsndisj  13636  incexc2  14490  lcmftp  15268  f1omvdco3  17785  psgnunilem4  17833  0ringnnzr  19183  gsumcom3  20119  mdetunilem7  20338  fctop  20713  cctop  20715  ntreq0  20786  ordtbas2  20900  cmpcld  21110  hausdiag  21353  fbun  21549  fbfinnfr  21550  opnfbas  21551  fbasrn  21593  filuni  21594  ufinffr  21638  alexsubALTlem2  21757  ellogdm  24280  usgredg2v  26006  2wspiundisj  26718  avril1  27167  shne0i  28147  chnlei  28184  cvnbtwn2  28986  cvnbtwn3  28987  cvnbtwn4  28988  chrelat2i  29064  atabs2i  29101  dmdbr5ati  29121  nmo  29165  disjdifprg  29224  eliccelico  29375  elicoelioo  29376  xrdifh  29378  f1ocnt  29392  tosglblem  29446  xrnarchi  29515  hasheuni  29920  cntnevol  30064  sitgaddlemb  30183  eulerpartlemgs2  30215  ballotlem2  30323  ballotlemodife  30332  plymulx0  30396  bnj1143  30561  bnj1304  30590  bnj1476  30617  bnj1533  30622  bnj1174  30771  bnj1204  30780  bnj1280  30788  erdszelem9  30881  dftr6  31339  fundmpss  31356  dfon2lem5  31381  dfon2lem8  31384  dfon2lem9  31385  wzel  31460  wzelOLD  31461  nosepon  31511  nodenselem7  31531  nocvxminlem  31534  elfuns  31637  dfrecs2  31672  gtinfOLD  31929  df3nandALT1  32011  andnand1  32013  imnand2  32014  bj-notalbii  32213  bj-cbvex2v  32353  fdc  33140  nninfnub  33146  tsbi4  33542  ts3an2  33557  ts3an3  33558  ts3or1  33559  n0el  33593  lcvnbtwn2  33761  lcvnbtwn3  33762  cvrnbtwn3  34010  dalem18  34414  lhpocnel2  34752  cdleme0nex  35024  cdlemk19w  35707  dihglblem6  36076  dvh2dim  36181  dvh3dim3N  36185  ctbnfien  36829  rencldnfilem  36831  numinfctb  37121  ifpnorcor  37273  ifpnancor  37274  ifpdfnan  37279  ifpananb  37299  ifpnannanb  37300  ifpxorxorb  37304  rp-fakenanass  37308  rp-isfinite6  37312  pwinfig  37314  elnonrel  37339  iunrelexp0  37442  frege131  37737  frege133  37739  compab  38094  zfregs2VD  38526  undif3VD  38568  onfrALTlem5VD  38571  sineq0ALT  38623  ndisj2  38670  disjrnmpt2  38816  uz0  39071  icccncfext  39372  itgioocnicc  39468  fourierdlem42  39641  fourierdlem62  39660  fourierdlem93  39691  fourierdlem101  39699  nsssmfmbf  40262  otiunsndisjX  40564  nltle2tri  40589  evennodd  40824  setrec2lem1  41688
  Copyright terms: Public domain W3C validator