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  nnmword  6795  brdifun  6838  swoer  6839  2dom  7097  pw2f1odclem  7138  php5  7163  php5dom  7168  findcard2s  7198  fimax2gtrilemstep  7209  fimax2gtri  7210  fidcenumlemrk  7276  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  9703  supinfneg  10011  infsupneg  10012  infregelbex  10014  eluzdc  10026  qapne  10055  xrltne  10232  xleneg  10256  nn0disj  10562  nelfzo  10576  elfzonelfzo  10665  fvinim0ffz  10677  zsupcllemstep  10679  zsupcllemex  10680  zsupssdc  10690  ioo0  10711  ico0  10713  ioc0  10714  flqlt  10738  expeq0  11028  nn0leexp2  11170  hashfibc  11305  leisorel  11311  wrdsymb0  11359  swrdnd  11453  maxleim  11994  maxabslemval  11997  maxleast  12002  minmax  12020  xrmaxleim  12035  xrmaxiflemval  12041  xrmaxlesup  12050  xrminmax  12056  summodclem3  12172  zeo3  12660  odd2np1  12665  mod2eq1n2dvds  12671  ndvdsadd  12723  fldivndvdslt  12729  bitsfval  12734  bitsval  12735  bits0  12740  bitsp1  12743  bitsmod  12748  bitscmp  12750  bitsinv1lem  12753  gcdneg  12784  nninfctlemfo  12842  algcvgblem  12852  lcmneg  12877  isprm3  12921  dvdsnprmd  12928  isprm5lem  12945  isprm5  12946  rpexp  12957  pwbdvdslemn  12969  pwbdvdseu  12972  nnmaxpwlemxy  12973  nnmaxpwlemparts  12977  nnmaxpw  12978  sqpweven  12980  2sqpwodd  12981  sqne2sq  12982  phiprmpw  13029  m1dvdsndvds  13056  pythagtrip  13091  pcgcd1  13136  prmpwdvds  13163  prmlem0  13249  prmlem1a  13250  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilem4  13299  ballotfilem7  13337  oddennn  13341  ctinfomlemom  13376  ctinfom  13377  isnsgrp  13780  nzrunit  14604  opprdrng  14729  bdxmet  15727  dedekindeulemlu  15847  suplociccex  15851  dedekindicclemlu  15856  efle  16002  logleb  16105  logdivle  16125  cxple  16152  cxple3  16156  zprmlogbaplem3  16217  zprmlogbap  16218  bposlem1  16311  lgsmod  16350  lgsdir2lem2  16353  lgsdir2  16357  lgsne0  16362  lgsprme0  16366  lgsquadlem1  16401  2lgslem3  16425  2lgsoddprm  16437  vtxd0nedgbfi  16745  1hevtxdg0fi  16753  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  eupth2lem3lem7fi  16920  eupth2lemsfi  16924  eupth2fi  16925  konigsberglem4  16937  decidi  17028  uzdcinzz  17031  bj-charfunbi  17042  bj-nalset  17126  bj-nnelirr  17184  subctctexmid  17235  exmidnotnotr  17241  exmidcon  17242  stnot  17244  wexmiddc  17247  nninfsellemeq  17263  ismkvnnlem  17309