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  2377  neeq2  2378  necon3abid  2403  neleq1  2463  neleq2  2464  cdeqnot  2973  ru  2984  sbcng  3026  sbcnel12g  3097  sbcne12g  3098  difjust  3154  eldif  3162  dfdif3  3269  difeq2  3271  disjne  3500  eldifpr  3645  eldiftp  3664  prel12  3797  nalset  4159  pwnss  4188  poeq1  4330  pocl  4334  swopo  4337  sotritrieq  4356  tz7.2  4385  regexmidlem1  4565  regexmid  4567  nordeq  4576  nlimsucg  4598  nndceq0  4650  nnregexmid  4653  poinxp  4728  posng  4731  intirr  5052  poirr2  5058  cnvpom  5208  fndmdif  5663  isopolem  5865  canth  5871  poxp  6285  nnmword  6571  brdifun  6614  swoer  6615  2dom  6859  pw2f1odclem  6890  php5  6914  php5dom  6919  findcard2s  6946  fimax2gtrilemstep  6956  fimax2gtri  6957  fidcenumlemrk  7013  supeq3  7049  supeq123d  7050  supmoti  7052  eqsupti  7055  supubti  7058  supsnti  7064  isotilem  7065  isoti  7066  supisolem  7067  supisoex  7068  cnvinfex  7077  cnvti  7078  eqinfti  7079  infvalti  7081  difinfsn  7159  ismkv  7212  ismkvnex  7214  mkvprop  7217  fodjumkvlemres  7218  enmkvlem  7220  onntri35  7297  onntri45  7301  tapeq1  7312  netap  7314  2omotaplemap  7317  exmidapne  7320  pitric  7381  addnidpig  7396  ltsonq  7458  elinp  7534  prltlu  7547  prdisj  7552  ltexprlemdisj  7666  suplocexpr  7785  ltposr  7823  aptisr  7839  suplocsrlem  7868  axpre-ltirr  7942  axpre-apti  7945  axpre-suploclemres  7961  axpre-suploc  7962  xrlenlt  8084  axapti  8090  axsuploc  8092  lttri3  8099  ltne  8104  leadd1  8449  reapti  8598  lemul1  8612  apirr  8624  apti  8641  apcon4bid  8643  lediv1  8888  lemuldiv  8900  lerec  8903  le2msq  8920  suprnubex  8972  suprleubex  8973  avgle1  9223  avgle2  9224  znnnlt1  9365  supinfneg  9660  infsupneg  9661  infregelbex  9663  eluzdc  9675  qapne  9704  xrltne  9879  xleneg  9903  nn0disj  10204  nelfzo  10218  elfzonelfzo  10297  fvinim0ffz  10308  ioo0  10328  ico0  10330  ioc0  10331  flqlt  10352  expeq0  10641  nn0leexp2  10781  leisorel  10908  wrdsymb0  10946  maxleim  11349  maxabslemval  11352  maxleast  11357  minmax  11373  xrmaxleim  11387  xrmaxiflemval  11393  xrmaxlesup  11402  xrminmax  11408  summodclem3  11523  zeo3  12009  odd2np1  12014  mod2eq1n2dvds  12020  ndvdsadd  12072  fldivndvdslt  12076  zsupcllemstep  12082  zsupcllemex  12083  zsupssdc  12091  gcdneg  12119  nninfctlemfo  12177  algcvgblem  12187  lcmneg  12212  isprm3  12256  dvdsnprmd  12263  isprm5lem  12279  isprm5  12280  rpexp  12291  pw2dvdslemn  12303  pw2dvdseu  12306  oddpwdclemxy  12307  oddpwdclemdc  12311  oddpwdc  12312  sqpweven  12313  2sqpwodd  12314  sqne2sq  12315  phiprmpw  12360  m1dvdsndvds  12386  pythagtrip  12421  pcgcd1  12466  prmpwdvds  12493  oddennn  12549  ctinfomlemom  12584  ctinfom  12585  isnsgrp  12989  nzrunit  13684  bdxmet  14669  dedekindeulemlu  14775  suplociccex  14779  dedekindicclemlu  14784  efle  14911  logleb  15010  cxple  15051  cxple3  15055  lgsmod  15142  lgsdir2lem2  15145  lgsdir2  15149  lgsne0  15154  lgsprme0  15158  lgsquadlem1  15191  decidi  15287  uzdcinzz  15290  bj-charfunbi  15303  bj-nalset  15387  bj-nnelirr  15445  subctctexmid  15491  nninfsellemeq  15504  ismkvnnlem  15542