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  2380  neeq2  2381  necon3abid  2406  neleq1  2466  neleq2  2467  cdeqnot  2977  ru  2988  sbcng  3030  sbcnel12g  3101  sbcne12g  3102  difjust  3158  eldif  3166  dfdif3  3274  difeq2  3276  disjne  3505  eldifpr  3650  eldiftp  3669  prel12  3802  nalset  4164  pwnss  4193  poeq1  4335  pocl  4339  swopo  4342  sotritrieq  4361  tz7.2  4390  regexmidlem1  4570  regexmid  4572  nordeq  4581  nlimsucg  4603  nndceq0  4655  nnregexmid  4658  poinxp  4733  posng  4736  intirr  5057  poirr2  5063  cnvpom  5213  fndmdif  5670  isopolem  5872  canth  5878  poxp  6299  nnmword  6585  brdifun  6628  swoer  6629  2dom  6873  pw2f1odclem  6904  php5  6928  php5dom  6933  findcard2s  6960  fimax2gtrilemstep  6970  fimax2gtri  6971  fidcenumlemrk  7029  supeq3  7065  supeq123d  7066  supmoti  7068  eqsupti  7071  supubti  7074  supsnti  7080  isotilem  7081  isoti  7082  supisolem  7083  supisoex  7084  cnvinfex  7093  cnvti  7094  eqinfti  7095  infvalti  7097  difinfsn  7175  ismkv  7228  ismkvnex  7230  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  onntri35  7322  onntri45  7326  tapeq1  7337  netap  7339  2omotaplemap  7342  exmidapne  7345  pitric  7407  addnidpig  7422  ltsonq  7484  elinp  7560  prltlu  7573  prdisj  7578  ltexprlemdisj  7692  suplocexpr  7811  ltposr  7849  aptisr  7865  suplocsrlem  7894  axpre-ltirr  7968  axpre-apti  7971  axpre-suploclemres  7987  axpre-suploc  7988  xrlenlt  8110  axapti  8116  axsuploc  8118  lttri3  8125  ltne  8130  leadd1  8476  reapti  8625  lemul1  8639  apirr  8651  apti  8668  apcon4bid  8670  lediv1  8915  lemuldiv  8927  lerec  8930  le2msq  8947  suprnubex  8999  suprleubex  9000  avgle1  9251  avgle2  9252  znnnlt1  9393  supinfneg  9688  infsupneg  9689  infregelbex  9691  eluzdc  9703  qapne  9732  xrltne  9907  xleneg  9931  nn0disj  10232  nelfzo  10246  elfzonelfzo  10325  fvinim0ffz  10336  zsupcllemstep  10338  zsupcllemex  10339  zsupssdc  10347  ioo0  10368  ico0  10370  ioc0  10371  flqlt  10392  expeq0  10681  nn0leexp2  10821  leisorel  10948  wrdsymb0  10986  maxleim  11389  maxabslemval  11392  maxleast  11397  minmax  11414  xrmaxleim  11428  xrmaxiflemval  11434  xrmaxlesup  11443  xrminmax  11449  summodclem3  11564  zeo3  12052  odd2np1  12057  mod2eq1n2dvds  12063  ndvdsadd  12115  fldivndvdslt  12121  bitsfval  12126  bitsval  12127  bits0  12132  bitsp1  12135  bitsmod  12140  bitscmp  12142  bitsinv1lem  12145  gcdneg  12176  nninfctlemfo  12234  algcvgblem  12244  lcmneg  12269  isprm3  12313  dvdsnprmd  12320  isprm5lem  12336  isprm5  12337  rpexp  12348  pw2dvdslemn  12360  pw2dvdseu  12363  oddpwdclemxy  12364  oddpwdclemdc  12368  oddpwdc  12369  sqpweven  12370  2sqpwodd  12371  sqne2sq  12372  phiprmpw  12417  m1dvdsndvds  12444  pythagtrip  12479  pcgcd1  12524  prmpwdvds  12551  oddennn  12636  ctinfomlemom  12671  ctinfom  12672  isnsgrp  13110  nzrunit  13822  bdxmet  14845  dedekindeulemlu  14965  suplociccex  14969  dedekindicclemlu  14974  efle  15120  logleb  15219  cxple  15261  cxple3  15265  lgsmod  15375  lgsdir2lem2  15378  lgsdir2  15382  lgsne0  15387  lgsprme0  15391  lgsquadlem1  15426  2lgslem3  15450  2lgsoddprm  15462  decidi  15549  uzdcinzz  15552  bj-charfunbi  15565  bj-nalset  15649  bj-nnelirr  15707  subctctexmid  15755  nninfsellemeq  15769  ismkvnnlem  15809