Theorem notbii 319

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 318	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	mpbi 229	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  sylnbi  329  xchnxbi  331  xchbinx  333  oplem1  1055  xorcomOLD  1513  xorbi12iOLD  1524  norcomOLD  1531  nic-axALT  1676  tbw-bijust  1700  rb-bijust  1751  19.43OLD  1886  cbvexvw  2040  hbn1fw  2048  hba1w  2050  exexw  2054  excom  2162  cbvrexf  3332  cgsex4g  3491  cbvrexcsf  3904  dfss4  4223  indifdirOLD  4250  neq0f  4306  n0el  4326  ab0ALT  4341  ab0orv  4343  abn0  4345  pssdifcom2  4453  difprsnss  4764  brdif  5163  otthne  5448  otiunsndisj  5482  difopab  5791  difopabOLD  5792  rexiunxp  5801  rexxpf  5808  rnep  5887  somin1  6092  cnvdif  6101  difxp  6121  imadif  6590  brprcneu  6837  brprcneuALT  6838  dffv2  6941  ovima0  7538  porpss  7669  tfinds  7801  poxp  8065  xpord2pred  8082  xpord2indlem  8084  tz7.48lem  8392  brsdom  8922  brsdom2  9048  unfi  9123  fimax2g  9240  ordunifi  9244  dfsup2  9389  supgtoreq  9415  infcllem  9432  suc11reg  9564  rankxplim2  9825  rankxplim3  9826  alephval3  10055  kmlem4  10098  cflim2  10208  isfin4-2  10259  fin23lem25  10269  fin1a2lem5  10349  fin12  10358  axcclem  10402  zorng  10449  infinf  10511  alephadd  10522  fpwwe2  10588  axpre-lttri  11110  dfinfre  12145  infrenegsup  12147  arch  12419  rpneg  12956  xmulcom  13195  xmulneg1  13198  xmulf  13201  xrinfmss2  13240  difreicc  13411  fzp1nel  13535  ssnn0fi  13900  fsuppmapnn0fiubex  13907  hashfun  14347  swrdccatin2  14629  s3iunsndisj  14865  incexc2  15734  lcmftp  16523  f1omvdco3  19245  psgnunilem4  19293  gsumcom3  19769  gsumxp2  19771  0ringnnzr  20212  mdetunilem7  22004  fctop  22391  cctop  22393  ntreq0  22465  ordtbas2  22579  cmpcld  22790  hausdiag  23033  fbun  23228  fbfinnfr  23229  opnfbas  23230  fbasrn  23272  filuni  23273  ufinffr  23317  alexsubALTlem2  23436  ellogdm  26031  nosepon  27050  noextenddif  27053  nomaxmo  27083  nosupinfsep  27117  nocvxminlem  27160  numedglnl  28158  usgredg2v  28238  clwwlknon1nloop  29106  avril1  29470  shne0i  30453  chnlei  30490  cvnbtwn2  31292  cvnbtwn3  31293  cvnbtwn4  31294  chrelat2i  31370  atabs2i  31407  dmdbr5ati  31427  nmo  31482  disjdifprg  31560  eliccelico  31748  elicoelioo  31749  xrdifh  31751  f1ocnt  31773  tosglblem  31904  xrnarchi  32090  hasheuni  32773  cntnevol  32916  sitgaddlemb  33037  eulerpartlemgs2  33069  ballotlem2  33177  ballotlemodife  33186  plymulx0  33248  bnj1143  33491  bnj1304  33520  bnj1476  33548  bnj1533  33553  bnj1174  33704  bnj1204  33713  bnj1280  33721  nummin  33784  0nn0m1nnn0  33792  lfuhgr3  33800  erdszelem9  33880  fmla0disjsuc  34079  dftr6  34410  fundmpss  34427  dfon2lem5  34448  dfon2lem8  34451  dfon2lem9  34452  wzel  34485  elfuns  34576  dfrecs2  34611  df3nandALT1  34947  andnand1  34949  imnand2  34950  bj-notalbii  35155  difunieq  35918  domalom  35948  fvineqsneq  35956  fdc  36277  nninfnub  36283  tsbi4  36668  ts3an2  36683  ts3an3  36684  ts3or1  36685  vvdifopab  36793  brvvdif  36796  n0elqs  36860  dfssr2  37034  lcvnbtwn2  37562  lcvnbtwn3  37563  cvrnbtwn3  37811  dalem18  38217  lhpocnel2  38555  cdleme0nex  38826  cdlemk19w  39508  dihglblem6  39876  dvh2dim  39981  dvh3dim3N  39985  aks4d1p7  40613  sticksstones1  40627  metakunt1  40650  ctbnfien  41199  rencldnfilem  41201  numinfctb  41488  onmaxnelsup  41615  onsupnmax  41620  onsupuni  41621  onsupeqnmax  41639  oenassex  41711  naddgeoa  41788  ifpnorcor  41874  ifpnancor  41875  ifpdfnan  41880  ifpananb  41900  ifpnannanb  41901  ifpxorxorb  41905  rp-isfinite6  41912  pwinfig  41955  elnonrel  41979  iunrelexp0  42096  frege131  42388  frege133  42390  compab  42844  zfregs2VD  43245  undif3VD  43286  sineq0ALT  43341  ndisj2  43381  ralfal  43498  uz0  43767  icccncfext  44248  itgioocnicc  44338  fourierdlem42  44510  fourierdlem62  44529  fourierdlem93  44560  fourierdlem101  44568  nsssmfmbf  45140  aiotavb  45442  afv2ndeffv0  45612  otiunsndisjX  45631  nltle2tri  45665  0nelsetpreimafv  45702  evennodd  45955