Theorem notbid 668

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 667	. 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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  833  dcbid  839  con1biidc  878  pm4.54dc  903  xorbi2d  1391  xorbi1d  1392  pm5.18im  1396  pm5.24dc  1409  neeq1  2373  neeq2  2374  necon3abid  2399  neleq1  2459  neleq2  2460  cdeqnot  2965  ru  2976  sbcng  3018  sbcnel12g  3089  sbcne12g  3090  difjust  3145  eldif  3153  dfdif3  3260  difeq2  3262  disjne  3491  eldifpr  3634  eldiftp  3653  prel12  3786  nalset  4148  pwnss  4177  poeq1  4317  pocl  4321  swopo  4324  sotritrieq  4343  tz7.2  4372  regexmidlem1  4550  regexmid  4552  nordeq  4561  nlimsucg  4583  nndceq0  4635  nnregexmid  4638  poinxp  4713  posng  4716  intirr  5033  poirr2  5039  cnvpom  5189  fndmdif  5642  isopolem  5844  canth  5850  poxp  6257  nnmword  6543  brdifun  6586  swoer  6587  2dom  6831  pw2f1odclem  6862  php5  6886  php5dom  6891  findcard2s  6918  fimax2gtrilemstep  6928  fimax2gtri  6929  fidcenumlemrk  6983  supeq3  7019  supeq123d  7020  supmoti  7022  eqsupti  7025  supubti  7028  supsnti  7034  isotilem  7035  isoti  7036  supisolem  7037  supisoex  7038  cnvinfex  7047  cnvti  7048  eqinfti  7049  infvalti  7051  difinfsn  7129  ismkv  7181  ismkvnex  7183  mkvprop  7186  fodjumkvlemres  7187  enmkvlem  7189  onntri35  7266  onntri45  7270  tapeq1  7281  netap  7283  2omotaplemap  7286  exmidapne  7289  pitric  7350  addnidpig  7365  ltsonq  7427  elinp  7503  prltlu  7516  prdisj  7521  ltexprlemdisj  7635  suplocexpr  7754  ltposr  7792  aptisr  7808  suplocsrlem  7837  axpre-ltirr  7911  axpre-apti  7914  axpre-suploclemres  7930  axpre-suploc  7931  xrlenlt  8052  axapti  8058  axsuploc  8060  lttri3  8067  ltne  8072  leadd1  8417  reapti  8566  lemul1  8580  apirr  8592  apti  8609  apcon4bid  8611  lediv1  8856  lemuldiv  8868  lerec  8871  le2msq  8888  suprnubex  8940  suprleubex  8941  avgle1  9189  avgle2  9190  znnnlt1  9331  supinfneg  9625  infsupneg  9626  infregelbex  9628  eluzdc  9640  qapne  9669  xrltne  9843  xleneg  9867  nn0disj  10168  elfzonelfzo  10260  fvinim0ffz  10271  ioo0  10290  ico0  10292  ioc0  10293  flqlt  10314  expeq0  10582  nn0leexp2  10722  leisorel  10849  maxleim  11246  maxabslemval  11249  maxleast  11254  minmax  11270  xrmaxleim  11284  xrmaxiflemval  11290  xrmaxlesup  11299  xrminmax  11305  summodclem3  11420  zeo3  11905  odd2np1  11910  mod2eq1n2dvds  11916  ndvdsadd  11968  fldivndvdslt  11972  zsupcllemstep  11978  zsupcllemex  11979  zsupssdc  11987  gcdneg  12015  algcvgblem  12081  lcmneg  12106  isprm3  12150  dvdsnprmd  12157  isprm5lem  12173  isprm5  12174  rpexp  12185  pw2dvdslemn  12197  pw2dvdseu  12200  oddpwdclemxy  12201  oddpwdclemdc  12205  oddpwdc  12206  sqpweven  12207  2sqpwodd  12208  sqne2sq  12209  phiprmpw  12254  m1dvdsndvds  12280  pythagtrip  12315  pcgcd1  12360  prmpwdvds  12387  oddennn  12443  ctinfomlemom  12478  ctinfom  12479  isnsgrp  12869  nzrunit  13535  bdxmet  14458  dedekindeulemlu  14556  suplociccex  14560  dedekindicclemlu  14565  efle  14654  logleb  14753  cxple  14794  cxple3  14798  lgsmod  14885  lgsdir2lem2  14888  lgsdir2  14892  lgsne0  14897  lgsprme0  14901  decidi  15005  uzdcinzz  15008  bj-charfunbi  15021  bj-nalset  15105  bj-nnelirr  15163  subctctexmid  15209  nninfsellemeq  15222  ismkvnnlem  15259