Theorem notbid 677

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 676	. 2 ⊢ ((𝜓 ↔ 𝜒) → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  annotanannot  680  stbid  844  dcbid  850  con1biidc  889  pm4.54dc  914  ifpbi123d  1005  xorbi2d  1429  xorbi1d  1430  pm5.18im  1434  pm5.24dc  1447  neeq1  2433  neeq2  2434  necon3abid  2459  neleq1  2519  neleq2  2520  cdeqnot  3039  ru  3050  sbcng  3092  sbcnel12g  3164  sbcne12g  3165  difjust  3221  eldif  3229  dfdif3  3339  difeq2  3341  disjne  3578  ifeqeqxdc  3687  eldifpr  3736  eldiftp  3755  prel12  3896  nalset  4265  pwnss  4298  poeq1  4446  pocl  4450  swopo  4453  sotritrieq  4472  tz7.2  4501  regexmidlem1  4682  regexmid  4684  nordeq  4693  nlimsucg  4715  nndceq0  4767  nnregexmid  4770  poinxp  4846  posng  4849  intirr  5177  poirr2  5183  cnvpom  5333  fndmdif  5817  isopolem  6031  canth  6039  poxp  6472  suppinisegdc  6513  nnmword  6796  brdifun  6839  swoer  6840  2dom  7099  pw2f1odclem  7140  php5  7165  php5dom  7170  findcard2s  7200  fimax2gtrilemstep  7211  fimax2gtri  7212  fidcenumlemrk  7278  supeq3  7336  supeq123d  7337  supmoti  7339  eqsupti  7342  supubti  7345  supsnti  7351  isotilem  7352  isoti  7353  supisolem  7354  supisoex  7355  cnvinfex  7364  cnvti  7365  eqinfti  7366  infvalti  7368  difinfsn  7446  ismkv  7499  ismkvnex  7501  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  onntri35  7602  onntri45  7606  papeq1  7615  papirr  7617  tapeq1  7624  netap  7626  2omotaplemap  7629  exmidapne  7632  pitric  7694  addnidpig  7709  ltsonq  7771  elinp  7847  prltlu  7860  prdisj  7865  ltexprlemdisj  7979  suplocexpr  8098  ltposr  8136  aptisr  8152  suplocsrlem  8181  axpre-ltirr  8255  axpre-apti  8258  axpre-suploclemres  8274  axpre-suploc  8275  xrlenlt  8396  axapti  8402  axsuploc  8404  lttri3  8411  ltne  8416  leadd1  8765  reapti  8915  lemul1  8929  apirr  8941  apti  8958  apcon4bid  8960  lediv1  9207  lemuldiv  9219  lerec  9222  le2msq  9239  suprnubex  9291  suprleubex  9292  avgle1  9557  avgle2  9558  znnnlt1  9701  supinfneg  10010  infsupneg  10011  infregelbex  10013  eluzdc  10025  qapne  10054  xrltne  10231  xleneg  10255  nn0disj  10561  nelfzo  10575  elfzonelfzo  10664  fvinim0ffz  10676  zsupcllemstep  10678  zsupcllemex  10679  zsupssdc  10689  ioo0  10710  ico0  10712  ioc0  10713  flqlt  10737  expeq0  11027  nn0leexp2  11169  hashfibc  11304  leisorel  11310  wrdsymb0  11358  swrdnd  11452  maxleim  11993  maxabslemval  11996  maxleast  12001  minmax  12019  xrmaxleim  12034  xrmaxiflemval  12040  xrmaxlesup  12049  xrminmax  12055  summodclem3  12171  zeo3  12659  odd2np1  12664  mod2eq1n2dvds  12670  ndvdsadd  12722  fldivndvdslt  12728  bitsfval  12733  bitsval  12734  bits0  12739  bitsp1  12742  bitsmod  12747  bitscmp  12749  bitsinv1lem  12752  gcdneg  12783  nninfctlemfo  12841  algcvgblem  12851  lcmneg  12876  isprm3  12920  dvdsnprmd  12927  isprm5lem  12944  isprm5  12945  rpexp  12956  pwbdvdslemn  12968  pwbdvdseu  12971  nnmaxpwlemxy  12972  nnmaxpwlemparts  12976  nnmaxpw  12977  sqpweven  12979  2sqpwodd  12980  sqne2sq  12981  phiprmpw  13028  m1dvdsndvds  13055  pythagtrip  13090  pcgcd1  13135  prmpwdvds  13162  prmlem0  13248  prmlem1a  13249  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemodife  13297  ballotfilem4  13298  ballotfilem7  13336  oddennn  13340  ctinfomlemom  13375  ctinfom  13376  isnsgrp  13779  nzrunit  14603  opprdrng  14728  bdxmet  15744  dedekindeulemlu  15864  suplociccex  15868  dedekindicclemlu  15873  efle  16019  logleb  16122  logdivle  16142  cxple  16169  cxple3  16173  zprmlogbaplem3  16234  zprmlogbap  16235  bposlem1  16328  lgsmod  16367  lgsdir2lem2  16370  lgsdir2  16374  lgsne0  16379  lgsprme0  16383  lgsquadlem1  16418  2lgslem3  16442  2lgsoddprm  16454  vtxd0nedgbfi  16762  1hevtxdg0fi  16770  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  eupth2lem3lem7fi  16937  eupth2lemsfi  16941  eupth2fi  16942  konigsberglem4  16954  decidi  17045  uzdcinzz  17048  bj-charfunbi  17059  bj-nalset  17143  bj-nnelirr  17201  subctctexmid  17252  exmidnotnotr  17258  exmidcon  17259  stnot  17261  wexmiddc  17264  nninfsellemeq  17280  ismkvnnlem  17326