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  1027  xorcom  1507  xorbi12i  1517  nic-axALT  1639  tbw-bijust  1663  rb-bijust  1714  19.43OLD  1851  cbvexvw  2012  hbn1fw  2014  hba1w  2016  excom  2082  cbvexv1  2212  cbvex  2308  cbvexv  2311  cbvex2  2316  cbvrexf  3196  cbvrexcsf  3599  elsymdifxor  3883  symdifass  3886  dfss4  3891  indifdir  3916  neq0f  3959  n0el  3973  ab0  3984  pssdifcom2  4088  difprsnss  4361  brdif  4738  otiunsndisj  5009  difopab  5286  rexiunxp  5295  rexxpf  5302  somin1  5564  cnvdif  5574  difxp  5593  imadif  6011  brprcneu  6222  dffv2  6310  ovima0  6855  porpss  6983  tfinds  7101  poxp  7334  tz7.48lem  7581  brsdom  8020  brsdom2  8125  fimax2g  8247  ordunifi  8251  dfsup2  8391  supgtoreq  8417  infcllem  8434  suc11reg  8554  rankxplim2  8781  rankxplim3  8782  alephval3  8971  kmlem4  9013  cflim2  9123  isfin4-2  9174  fin23lem25  9184  fin1a2lem5  9264  fin12  9273  axcclem  9317  zorng  9364  infinf  9426  alephadd  9437  fpwwe2  9503  axpre-lttri  10024  dfinfre  11042  infrenegsup  11044  arch  11327  rpneg  11901  xmulcom  12134  xmulneg1  12137  xmulf  12140  xrinfmss2  12179  difreicc  12342  fzp1nel  12462  ssnn0fi  12824  fsuppmapnn0fiubex  12832  hashfun  13262  swrdccatin2  13533  s3iunsndisj  13753  incexc2  14614  lcmftp  15396  f1omvdco3  17915  psgnunilem4  17963  0ringnnzr  19317  gsumcom3  20253  mdetunilem7  20472  fctop  20856  cctop  20858  ntreq0  20929  ordtbas2  21043  cmpcld  21253  hausdiag  21496  fbun  21691  fbfinnfr  21692  opnfbas  21693  fbasrn  21735  filuni  21736  ufinffr  21780  alexsubALTlem2  21899  ellogdm  24430  numedglnl  26084  usgredg2v  26164  clwwlknon1nloop  27074  avril1  27449  shne0i  28435  chnlei  28472  cvnbtwn2  29274  cvnbtwn3  29275  cvnbtwn4  29276  chrelat2i  29352  atabs2i  29389  dmdbr5ati  29409  nmo  29453  difrab2  29465  disjdifprg  29514  eliccelico  29667  elicoelioo  29668  xrdifh  29670  f1ocnt  29687  tosglblem  29797  xrnarchi  29866  hasheuni  30275  cntnevol  30419  sitgaddlemb  30538  eulerpartlemgs2  30570  ballotlem2  30678  ballotlemodife  30687  plymulx0  30752  bnj1143  30987  bnj1304  31016  bnj1476  31043  bnj1533  31048  bnj1174  31197  bnj1204  31206  bnj1280  31214  erdszelem9  31307  dftr6  31766  fundmpss  31790  dfon2lem5  31816  dfon2lem8  31819  dfon2lem9  31820  wzel  31894  nosepon  31943  noextenddif  31946  nomaxmo  31972  nocvxminlem  32018  elfuns  32147  dfrecs2  32182  gtinfOLD  32439  df3nandALT1  32521  andnand1  32523  imnand2  32524  bj-notalbii  32723  bj-cbvex2v  32863  fdc  33671  nninfnub  33677  tsbi4  34073  ts3an2  34088  ts3an3  34089  ts3or1  34090  vvdifopab  34165  brvvdif  34168  n0elqs  34239  dfssr2  34389  lcvnbtwn2  34632  lcvnbtwn3  34633  cvrnbtwn3  34881  dalem18  35285  lhpocnel2  35623  cdleme0nex  35895  cdlemk19w  36577  dihglblem6  36946  dvh2dim  37051  dvh3dim3N  37055  ctbnfien  37699  rencldnfilem  37701  numinfctb  37990  ifpnorcor  38142  ifpnancor  38143  ifpdfnan  38148  ifpananb  38168  ifpnannanb  38169  ifpxorxorb  38173  rp-fakenanass  38177  rp-isfinite6  38181  pwinfig  38183  elnonrel  38208  iunrelexp0  38311  frege131  38605  frege133  38607  compab  38962  zfregs2VD  39390  undif3VD  39432  sineq0ALT  39487  ndisj2  39532  disjrnmpt2  39689  uz0  39952  icccncfext  40418  itgioocnicc  40511  fourierdlem42  40684  fourierdlem62  40703  fourierdlem93  40734  fourierdlem101  40742  nsssmfmbf  41308  otiunsndisjX  41621  nltle2tri  41648  evennodd  41881  setrec2lem1  42765
  Copyright terms: Public domain W3C validator