Theorem notbid 669

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 668	. 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  834  dcbid  840  con1biidc  879  pm4.54dc  904  xorbi2d  1400  xorbi1d  1401  pm5.18im  1405  pm5.24dc  1418  neeq1  2389  neeq2  2390  necon3abid  2415  neleq1  2475  neleq2  2476  cdeqnot  2986  ru  2997  sbcng  3039  sbcnel12g  3110  sbcne12g  3111  difjust  3167  eldif  3175  dfdif3  3283  difeq2  3285  disjne  3514  eldifpr  3660  eldiftp  3679  prel12  3812  nalset  4174  pwnss  4203  poeq1  4346  pocl  4350  swopo  4353  sotritrieq  4372  tz7.2  4401  regexmidlem1  4581  regexmid  4583  nordeq  4592  nlimsucg  4614  nndceq0  4666  nnregexmid  4669  poinxp  4744  posng  4747  intirr  5069  poirr2  5075  cnvpom  5225  fndmdif  5685  isopolem  5891  canth  5897  poxp  6318  nnmword  6604  brdifun  6647  swoer  6648  2dom  6897  pw2f1odclem  6931  php5  6955  php5dom  6960  findcard2s  6987  fimax2gtrilemstep  6997  fimax2gtri  6998  fidcenumlemrk  7056  supeq3  7092  supeq123d  7093  supmoti  7095  eqsupti  7098  supubti  7101  supsnti  7107  isotilem  7108  isoti  7109  supisolem  7110  supisoex  7111  cnvinfex  7120  cnvti  7121  eqinfti  7122  infvalti  7124  difinfsn  7202  ismkv  7255  ismkvnex  7257  mkvprop  7260  fodjumkvlemres  7261  enmkvlem  7263  onntri35  7349  onntri45  7353  tapeq1  7364  netap  7366  2omotaplemap  7369  exmidapne  7372  pitric  7434  addnidpig  7449  ltsonq  7511  elinp  7587  prltlu  7600  prdisj  7605  ltexprlemdisj  7719  suplocexpr  7838  ltposr  7876  aptisr  7892  suplocsrlem  7921  axpre-ltirr  7995  axpre-apti  7998  axpre-suploclemres  8014  axpre-suploc  8015  xrlenlt  8137  axapti  8143  axsuploc  8145  lttri3  8152  ltne  8157  leadd1  8503  reapti  8652  lemul1  8666  apirr  8678  apti  8695  apcon4bid  8697  lediv1  8942  lemuldiv  8954  lerec  8957  le2msq  8974  suprnubex  9026  suprleubex  9027  avgle1  9278  avgle2  9279  znnnlt1  9420  supinfneg  9716  infsupneg  9717  infregelbex  9719  eluzdc  9731  qapne  9760  xrltne  9935  xleneg  9959  nn0disj  10260  nelfzo  10274  elfzonelfzo  10359  fvinim0ffz  10370  zsupcllemstep  10372  zsupcllemex  10373  zsupssdc  10381  ioo0  10402  ico0  10404  ioc0  10405  flqlt  10426  expeq0  10715  nn0leexp2  10855  leisorel  10982  wrdsymb0  11026  swrdnd  11112  maxleim  11516  maxabslemval  11519  maxleast  11524  minmax  11541  xrmaxleim  11555  xrmaxiflemval  11561  xrmaxlesup  11570  xrminmax  11576  summodclem3  11691  zeo3  12179  odd2np1  12184  mod2eq1n2dvds  12190  ndvdsadd  12242  fldivndvdslt  12248  bitsfval  12253  bitsval  12254  bits0  12259  bitsp1  12262  bitsmod  12267  bitscmp  12269  bitsinv1lem  12272  gcdneg  12303  nninfctlemfo  12361  algcvgblem  12371  lcmneg  12396  isprm3  12440  dvdsnprmd  12447  isprm5lem  12463  isprm5  12464  rpexp  12475  pw2dvdslemn  12487  pw2dvdseu  12490  oddpwdclemxy  12491  oddpwdclemdc  12495  oddpwdc  12496  sqpweven  12497  2sqpwodd  12498  sqne2sq  12499  phiprmpw  12544  m1dvdsndvds  12571  pythagtrip  12606  pcgcd1  12651  prmpwdvds  12678  oddennn  12763  ctinfomlemom  12798  ctinfom  12799  isnsgrp  13238  nzrunit  13950  bdxmet  14973  dedekindeulemlu  15093  suplociccex  15097  dedekindicclemlu  15102  efle  15248  logleb  15347  cxple  15389  cxple3  15393  lgsmod  15503  lgsdir2lem2  15506  lgsdir2  15510  lgsne0  15515  lgsprme0  15519  lgsquadlem1  15554  2lgslem3  15578  2lgsoddprm  15590  decidi  15735  uzdcinzz  15738  bj-charfunbi  15751  bj-nalset  15835  bj-nnelirr  15893  subctctexmid  15941  nninfsellemeq  15955  ismkvnnlem  15995