Theorem notbid 667

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 666	. 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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  832  dcbid  838  con1biidc  877  pm4.54dc  902  xorbi2d  1380  xorbi1d  1381  pm5.18im  1385  pm5.24dc  1398  neeq1  2360  neeq2  2361  necon3abid  2386  neleq1  2446  neleq2  2447  cdeqnot  2951  ru  2962  sbcng  3004  sbcnel12g  3075  sbcne12g  3076  difjust  3131  eldif  3139  dfdif3  3246  difeq2  3248  disjne  3477  eldifpr  3620  eldiftp  3639  prel12  3772  nalset  4134  pwnss  4160  poeq1  4300  pocl  4304  swopo  4307  sotritrieq  4326  tz7.2  4355  regexmidlem1  4533  regexmid  4535  nordeq  4544  nlimsucg  4566  nndceq0  4618  nnregexmid  4621  poinxp  4696  posng  4699  intirr  5016  poirr2  5022  cnvpom  5172  fndmdif  5622  isopolem  5823  canth  5829  poxp  6233  nnmword  6519  brdifun  6562  swoer  6563  2dom  6805  php5  6858  php5dom  6863  findcard2s  6890  fimax2gtrilemstep  6900  fimax2gtri  6901  fidcenumlemrk  6953  supeq3  6989  supeq123d  6990  supmoti  6992  eqsupti  6995  supubti  6998  supsnti  7004  isotilem  7005  isoti  7006  supisolem  7007  supisoex  7008  cnvinfex  7017  cnvti  7018  eqinfti  7019  infvalti  7021  difinfsn  7099  ismkv  7151  ismkvnex  7153  mkvprop  7156  fodjumkvlemres  7157  enmkvlem  7159  onntri35  7236  onntri45  7240  tapeq1  7251  netap  7253  2omotaplemap  7256  exmidapne  7259  pitric  7320  addnidpig  7335  ltsonq  7397  elinp  7473  prltlu  7486  prdisj  7491  ltexprlemdisj  7605  suplocexpr  7724  ltposr  7762  aptisr  7778  suplocsrlem  7807  axpre-ltirr  7881  axpre-apti  7884  axpre-suploclemres  7900  axpre-suploc  7901  xrlenlt  8022  axapti  8028  axsuploc  8030  lttri3  8037  ltne  8042  leadd1  8387  reapti  8536  lemul1  8550  apirr  8562  apti  8579  apcon4bid  8581  lediv1  8826  lemuldiv  8838  lerec  8841  le2msq  8858  suprnubex  8910  suprleubex  8911  avgle1  9159  avgle2  9160  znnnlt1  9301  supinfneg  9595  infsupneg  9596  infregelbex  9598  eluzdc  9610  qapne  9639  xrltne  9813  xleneg  9837  nn0disj  10138  elfzonelfzo  10230  fvinim0ffz  10241  ioo0  10260  ico0  10262  ioc0  10263  flqlt  10283  expeq0  10551  nn0leexp2  10690  leisorel  10817  maxleim  11214  maxabslemval  11217  maxleast  11222  minmax  11238  xrmaxleim  11252  xrmaxiflemval  11258  xrmaxlesup  11267  xrminmax  11273  summodclem3  11388  zeo3  11873  odd2np1  11878  mod2eq1n2dvds  11884  ndvdsadd  11936  fldivndvdslt  11940  zsupcllemstep  11946  zsupcllemex  11947  zsupssdc  11955  gcdneg  11983  algcvgblem  12049  lcmneg  12074  isprm3  12118  dvdsnprmd  12125  isprm5lem  12141  isprm5  12142  rpexp  12153  pw2dvdslemn  12165  pw2dvdseu  12168  oddpwdclemxy  12169  oddpwdclemdc  12173  oddpwdc  12174  sqpweven  12175  2sqpwodd  12176  sqne2sq  12177  phiprmpw  12222  m1dvdsndvds  12248  pythagtrip  12283  pcgcd1  12327  prmpwdvds  12353  oddennn  12393  ctinfomlemom  12428  ctinfom  12429  isnsgrp  12812  nzrunit  13329  bdxmet  14004  dedekindeulemlu  14102  suplociccex  14106  dedekindicclemlu  14111  efle  14200  logleb  14299  cxple  14340  cxple3  14344  lgsmod  14430  lgsdir2lem2  14433  lgsdir2  14437  lgsne0  14442  lgsprme0  14446  decidi  14550  uzdcinzz  14553  bj-charfunbi  14566  bj-nalset  14650  bj-nnelirr  14708  subctctexmid  14753  nninfsellemeq  14766  ismkvnnlem  14803