Theorem notbid 671

Description: Equivalence property for negation. Deduction form. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
notbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
notbid	⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Proof of Theorem notbid

Step	Hyp	Ref	Expression
1		notbid.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		notbi 670	. 2 ⊢ ((𝜓 ↔ 𝜒) → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  837  dcbid  843  con1biidc  882  pm4.54dc  907  ifpbi123d  998  xorbi2d  1422  xorbi1d  1423  pm5.18im  1427  pm5.24dc  1440  neeq1  2413  neeq2  2414  necon3abid  2439  neleq1  2499  neleq2  2500  cdeqnot  3017  ru  3028  sbcng  3070  sbcnel12g  3142  sbcne12g  3143  difjust  3199  eldif  3207  dfdif3  3315  difeq2  3317  disjne  3546  eldifpr  3694  eldiftp  3713  prel12  3852  nalset  4217  pwnss  4247  poeq1  4394  pocl  4398  swopo  4401  sotritrieq  4420  tz7.2  4449  regexmidlem1  4629  regexmid  4631  nordeq  4640  nlimsucg  4662  nndceq0  4714  nnregexmid  4717  poinxp  4793  posng  4796  intirr  5121  poirr2  5127  cnvpom  5277  fndmdif  5748  isopolem  5958  canth  5964  poxp  6392  nnmword  6681  brdifun  6724  swoer  6725  2dom  6975  pw2f1odclem  7015  php5  7039  php5dom  7044  findcard2s  7072  fimax2gtrilemstep  7083  fimax2gtri  7084  fidcenumlemrk  7144  supeq3  7180  supeq123d  7181  supmoti  7183  eqsupti  7186  supubti  7189  supsnti  7195  isotilem  7196  isoti  7197  supisolem  7198  supisoex  7199  cnvinfex  7208  cnvti  7209  eqinfti  7210  infvalti  7212  difinfsn  7290  ismkv  7343  ismkvnex  7345  mkvprop  7348  fodjumkvlemres  7349  enmkvlem  7351  onntri35  7445  onntri45  7449  tapeq1  7461  netap  7463  2omotaplemap  7466  exmidapne  7469  pitric  7531  addnidpig  7546  ltsonq  7608  elinp  7684  prltlu  7697  prdisj  7702  ltexprlemdisj  7816  suplocexpr  7935  ltposr  7973  aptisr  7989  suplocsrlem  8018  axpre-ltirr  8092  axpre-apti  8095  axpre-suploclemres  8111  axpre-suploc  8112  xrlenlt  8234  axapti  8240  axsuploc  8242  lttri3  8249  ltne  8254  leadd1  8600  reapti  8749  lemul1  8763  apirr  8775  apti  8792  apcon4bid  8794  lediv1  9039  lemuldiv  9051  lerec  9054  le2msq  9071  suprnubex  9123  suprleubex  9124  avgle1  9375  avgle2  9376  znnnlt1  9517  supinfneg  9819  infsupneg  9820  infregelbex  9822  eluzdc  9834  qapne  9863  xrltne  10038  xleneg  10062  nn0disj  10363  nelfzo  10377  elfzonelfzo  10465  fvinim0ffz  10477  zsupcllemstep  10479  zsupcllemex  10480  zsupssdc  10488  ioo0  10509  ico0  10511  ioc0  10512  flqlt  10533  expeq0  10822  nn0leexp2  10962  leisorel  11091  wrdsymb0  11136  swrdnd  11230  maxleim  11756  maxabslemval  11759  maxleast  11764  minmax  11781  xrmaxleim  11795  xrmaxiflemval  11801  xrmaxlesup  11810  xrminmax  11816  summodclem3  11931  zeo3  12419  odd2np1  12424  mod2eq1n2dvds  12430  ndvdsadd  12482  fldivndvdslt  12488  bitsfval  12493  bitsval  12494  bits0  12499  bitsp1  12502  bitsmod  12507  bitscmp  12509  bitsinv1lem  12512  gcdneg  12543  nninfctlemfo  12601  algcvgblem  12611  lcmneg  12636  isprm3  12680  dvdsnprmd  12687  isprm5lem  12703  isprm5  12704  rpexp  12715  pw2dvdslemn  12727  pw2dvdseu  12730  oddpwdclemxy  12731  oddpwdclemdc  12735  oddpwdc  12736  sqpweven  12737  2sqpwodd  12738  sqne2sq  12739  phiprmpw  12784  m1dvdsndvds  12811  pythagtrip  12846  pcgcd1  12891  prmpwdvds  12918  oddennn  13003  ctinfomlemom  13038  ctinfom  13039  isnsgrp  13479  nzrunit  14192  bdxmet  15215  dedekindeulemlu  15335  suplociccex  15339  dedekindicclemlu  15344  efle  15490  logleb  15589  cxple  15631  cxple3  15635  lgsmod  15745  lgsdir2lem2  15748  lgsdir2  15752  lgsne0  15757  lgsprme0  15761  lgsquadlem1  15796  2lgslem3  15820  2lgsoddprm  15832  vtxd0nedgbfi  16105  1hevtxdg0fi  16113  decidi  16327  uzdcinzz  16330  bj-charfunbi  16342  bj-nalset  16426  bj-nnelirr  16484  subctctexmid  16537  nninfsellemeq  16552  ismkvnnlem  16592