Theorem notbii 323

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

Step	Hyp	Ref	Expression
1		notbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		notbi 322	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	mpbi 233	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sylnbi  333  xchnxbi  335  xchbinx  337  oplem1  1072  nic-axALT  1706  tbw-bijust  1730  rb-bijust  1781  19.43OLD  1915  cbvexvw  2069  hbn1fw  2079  hba1w  2081  exexw  2085  excom  2198  cbvrexf  3346  cbvrexcsf  3890  dfss4  4213  neq0f  4294  n0el  4311  ab0ALT  4329  abn0  4333  pssdifcom2  4445  difprsnss  4758  brdif  5157  otthne  5455  otiunsndisj  5493  difopab  5809  rexiunxp  5818  rexxpf  5826  dm0rn0  5907  rnep  5910  somin1  6129  cnvdif  6136  difxp  6157  xpdifcnvepel  6162  imadif  6629  brprcneu  6880  brprcneuALT  6881  dffv2  6985  ovima0  7604  porpss  7747  tfinds  7875  poxp  8147  xpord2pred  8169  xpord2indlem  8171  tz7.48lemOLD  8459  brsdom  9009  brsdom2  9128  unfi  9194  fimax2g  9285  ordunifi  9289  dfsup2  9443  supgtoreq  9470  infcllem  9487  suc11reg  9627  rankxplim2  9904  rankxplim3  9905  alephval3  10196  kmlem4  10239  cflim2  10348  isfin4-2  10399  fin23lem25  10409  fin1a2lem5  10489  fin12  10498  axcclem  10542  zorng  10589  alephadd  10669  fpwwe2  10735  axpre-lttri  11257  dfinfre  12305  infrenegsup  12307  arch  12610  0nn0m1nnn0  12760  rpneg  13161  xmulcom  13403  xmulneg1  13406  xmulf  13409  xrinfmss2  13448  difreicc  13622  fzp1nel  13752  ssnn0fi  14135  fsuppmapnn0fiubex  14142  hashfun  14589  swrdccatin2  14886  s3iunsndisj  15130  incexc2  16016  lcmftp  16820  f1omvdco3  19672  psgnunilem4  19720  gsumcom3  20201  gsumxp2  20203  0ringnnzr  20785  mdetunilem7  22942  fctop  23331  cctop  23333  ntreq0  23404  ordtbas2  23518  cmpcld  23729  hausdiag  23973  fbun  24168  fbfinnfr  24169  opnfbas  24170  fbasrn  24212  filuni  24213  ufinffr  24257  alexsubALTlem2  24376  plyn0mulidp  26611  ellogdm  26976  nosepon  28031  noextenddif  28034  nomaxmo  28064  nosupinfsep  28098  nocvxminlem  28149  bdayfinbndlem1  28862  numedglnl  29731  lfuhgr3  29737  usgredg2v  29817  clwwlknon1nloop  30699  avril1  31073  shne0i  32059  chnlei  32096  cvnbtwn2  32898  cvnbtwn3  32899  cvnbtwn4  32900  chrelat2i  32976  atabs2i  33013  dmdbr5ati  33033  nmo  33137  disjdifprg  33220  eliccelico  33419  elicoelioo  33420  xrdifh  33422  f1ocnt  33442  tosglblem  33585  xrnarchi  33795  elrgspnlem2  33854  fldextrspunlsplem  34355  hasheuni  34767  cntnevol  34911  sitgaddlemb  35030  eulerpartlemgs2  35062  ballotlem2  35171  ballotlemodife  35180  bnj1143  35470  bnj1304  35499  bnj1476  35527  bnj1533  35532  bnj1174  35683  bnj1204  35692  bnj1280  35700  rmo6  35760  nummin  35780  axreg  35863  axregscl  35864  noinfepregs  35869  axregs  35875  kardexen  35899  vonf1wev  35987  vonf1owevOLD  35989  erdszelem9  36082  fmla0disjsuc  36281  mirimanoffr  36578  dftr6  36640  fundmpss  36656  dfon2lem5  36673  dfon2lem8  36676  dfon2lem9  36677  wzel  36710  elfuns  36801  dfrecs2  36838  dffr7  36844  df3nandALT1  37311  andnand1  37313  imnand2  37314  regsfromregtco  37450  regsfromunir1  37452  bj-notalbii  37623  difunieq  38434  domalom  38464  fvineqsneq  38472  fdc  38816  nninfnub  38822  tsbi4  39205  ts3an2  39220  ts3an3  39221  ts3or1  39222  vvdifopab  39334  brvvdif  39337  n0elqs  39401  dfssr2  39648  lcvnbtwn2  40221  lcvnbtwn3  40222  cvrnbtwn3  40470  dalem18  40875  lhpocnel2  41213  cdleme0nex  41484  cdlemk19w  42166  dihglblem6  42534  dvh2dim  42639  dvh3dim3N  42643  aks4d1p7  43270  aks6d1c5  43326  sticksstones1  43333  aks6d1c6lem3  43359  redvmptabs  43548  ctbnfien  43962  rencldnfilem  43964  numinfctb  44242  onmaxnelsup  44362  onsupnmax  44367  onsupuni  44368  onsupeqnmax  44386  oenassex  44457  naddgeoa  44533  ifpnorcor  44618  ifpnancor  44619  ifpdfnan  44624  ifpananb  44644  ifpnannanb  44645  ifpxorxorb  44649  rp-isfinite6  44656  pwinfig  44699  elnonrel  44723  iunrelexp0  44839  frege131  45131  frege133  45133  compab  45561  zfregs2VD  45959  undif3VD  46000  sineq0ALT  46055  rext0  46057  permac8prim  46140  ndisj2  46204  ralfal  46312  uz0  46558  icccncfext  47033  itgioocnicc  47123  fourierdlem42  47295  fourierdlem62  47314  fourierdlem93  47345  fourierdlem101  47353  nsssmfmbf  47925  aiotavb  48296  afv2ndeffv0  48466  otiunsndisjX  48485  nltle2tri  48519  0nelsetpreimafv  48608  evennodd  48877