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 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  319  xchnxbi  321  xchbinx  323  oplem1  1043  xorcom  1615  xorbi12i  1625  nic-axALT  1747  tbw-bijust  1771  rb-bijust  1822  19.43OLD  1963  cbvexvw  2126  hbn1fw  2129  hba1w  2131  excom  2198  cbvexv1  2337  cbvrexf  3315  cbvrexcsf  3716  elsymdifxor  4000  symdifass  4003  dfss4  4008  indifdir  4033  neq0f  4075  n0el  4088  ab0  4099  pssdifcom2  4198  difprsnss  4466  brdif  4840  otiunsndisj  5114  difopab  5393  rexiunxp  5402  rexxpf  5409  somin1  5671  cnvdif  5681  difxp  5700  imadif  6114  brprcneu  6326  dffv2  6414  ovima0  6961  porpss  7089  tfinds  7207  poxp  7441  tz7.48lem  7690  brsdom  8133  brsdom2  8241  fimax2g  8363  ordunifi  8367  dfsup2  8507  supgtoreq  8533  infcllem  8550  suc11reg  8681  rankxplim2  8908  rankxplim3  8909  alephval3  9134  kmlem4  9178  cflim2  9288  isfin4-2  9339  fin23lem25  9349  fin1a2lem5  9429  fin12  9438  axcclem  9482  zorng  9529  infinf  9591  alephadd  9602  fpwwe2  9668  axpre-lttri  10189  dfinfre  11207  infrenegsup  11209  arch  11492  rpneg  12067  xmulcom  12302  xmulneg1  12305  xmulf  12308  xrinfmss2  12347  difreicc  12512  fzp1nel  12632  ssnn0fi  12993  fsuppmapnn0fiubex  13000  hashfun  13427  swrdccatin2  13697  s3iunsndisj  13918  incexc2  14778  lcmftp  15558  f1omvdco3  18077  psgnunilem4  18125  0ringnnzr  19485  gsumcom3  20423  mdetunilem7  20643  fctop  21030  cctop  21032  ntreq0  21103  ordtbas2  21217  cmpcld  21427  hausdiag  21670  fbun  21865  fbfinnfr  21866  opnfbas  21867  fbasrn  21909  filuni  21910  ufinffr  21954  alexsubALTlem2  22073  ellogdm  24607  numedglnl  26262  usgredg2v  26342  clwwlknon1nloop  27275  avril1  27662  shne0i  28648  chnlei  28685  cvnbtwn2  29487  cvnbtwn3  29488  cvnbtwn4  29489  chrelat2i  29565  atabs2i  29602  dmdbr5ati  29622  nmo  29666  difrab2  29678  disjdifprg  29727  eliccelico  29880  elicoelioo  29881  xrdifh  29883  f1ocnt  29900  tosglblem  30010  xrnarchi  30079  hasheuni  30488  cntnevol  30632  sitgaddlemb  30751  eulerpartlemgs2  30783  ballotlem2  30891  ballotlemodife  30900  plymulx0  30965  bnj1143  31200  bnj1304  31229  bnj1476  31256  bnj1533  31261  bnj1174  31410  bnj1204  31419  bnj1280  31427  erdszelem9  31520  dftr6  31979  fundmpss  32003  dfon2lem5  32029  dfon2lem8  32032  dfon2lem9  32033  wzel  32107  nosepon  32156  noextenddif  32159  nomaxmo  32185  nocvxminlem  32231  elfuns  32360  dfrecs2  32395  gtinfOLD  32652  df3nandALT1  32734  andnand1  32736  imnand2  32737  bj-notalbii  32936  bj-cbvex2v  33075  fdc  33874  nninfnub  33880  tsbi4  34276  ts3an2  34291  ts3an3  34292  ts3or1  34293  vvdifopab  34368  brvvdif  34371  n0elqs  34442  dfssr2  34592  lcvnbtwn2  34837  lcvnbtwn3  34838  cvrnbtwn3  35086  dalem18  35490  lhpocnel2  35828  cdleme0nex  36100  cdlemk19w  36782  dihglblem6  37151  dvh2dim  37256  dvh3dim3N  37260  ctbnfien  37909  rencldnfilem  37911  numinfctb  38200  ifpnorcor  38352  ifpnancor  38353  ifpdfnan  38358  ifpananb  38378  ifpnannanb  38379  ifpxorxorb  38383  rp-fakenanass  38387  rp-isfinite6  38391  pwinfig  38393  elnonrel  38418  iunrelexp0  38521  frege131  38815  frege133  38817  compab  39172  zfregs2VD  39599  undif3VD  39641  sineq0ALT  39696  ndisj2  39740  disjrnmpt2  39896  uz0  40156  icccncfext  40619  itgioocnicc  40711  fourierdlem42  40884  fourierdlem62  40903  fourierdlem93  40934  fourierdlem101  40942  nsssmfmbf  41508  otiunsndisjX  41822  nltle2tri  41852  evennodd  42085  setrec2lem1  42969
  Copyright terms: Public domain W3C validator