Theorem notbid 662

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  827  dcbid  833  con1biidc  872  pm4.54dc  897  xorbi2d  1375  xorbi1d  1376  pm5.18im  1380  pm5.24dc  1393  neeq1  2353  neeq2  2354  necon3abid  2379  neleq1  2439  neleq2  2440  cdeqnot  2943  ru  2954  sbcng  2995  sbcnel12g  3066  sbcne12g  3067  difjust  3122  eldif  3130  dfdif3  3237  difeq2  3239  disjne  3467  eldifpr  3608  eldiftp  3627  prel12  3756  nalset  4117  pwnss  4143  poeq1  4282  pocl  4286  swopo  4289  sotritrieq  4308  tz7.2  4337  regexmidlem1  4515  regexmid  4517  nordeq  4526  nlimsucg  4548  nndceq0  4600  nnregexmid  4603  poinxp  4678  posng  4681  intirr  4995  poirr2  5001  cnvpom  5151  fndmdif  5598  isopolem  5798  canth  5804  poxp  6208  nnmword  6494  brdifun  6536  swoer  6537  2dom  6779  php5  6832  php5dom  6837  findcard2s  6864  fimax2gtrilemstep  6874  fimax2gtri  6875  fidcenumlemrk  6927  supeq3  6963  supeq123d  6964  supmoti  6966  eqsupti  6969  supubti  6972  supsnti  6978  isotilem  6979  isoti  6980  supisolem  6981  supisoex  6982  cnvinfex  6991  cnvti  6992  eqinfti  6993  infvalti  6995  difinfsn  7073  ismkv  7125  ismkvnex  7127  mkvprop  7130  fodjumkvlemres  7131  enmkvlem  7133  onntri35  7201  onntri45  7205  pitric  7270  addnidpig  7285  ltsonq  7347  elinp  7423  prltlu  7436  prdisj  7441  ltexprlemdisj  7555  suplocexpr  7674  ltposr  7712  aptisr  7728  suplocsrlem  7757  axpre-ltirr  7831  axpre-apti  7834  axpre-suploclemres  7850  axpre-suploc  7851  xrlenlt  7971  axapti  7977  axsuploc  7979  lttri3  7986  ltne  7991  leadd1  8336  reapti  8485  lemul1  8499  apirr  8511  apti  8528  apcon4bid  8530  lediv1  8772  lemuldiv  8784  lerec  8787  le2msq  8804  suprnubex  8856  suprleubex  8857  avgle1  9105  avgle2  9106  znnnlt1  9247  supinfneg  9541  infsupneg  9542  infregelbex  9544  eluzdc  9556  qapne  9585  xrltne  9757  xleneg  9781  nn0disj  10081  elfzonelfzo  10173  fvinim0ffz  10184  ioo0  10203  ico0  10205  ioc0  10206  flqlt  10226  expeq0  10494  nn0leexp2  10632  leisorel  10759  maxleim  11156  maxabslemval  11159  maxleast  11164  minmax  11180  xrmaxleim  11194  xrmaxiflemval  11200  xrmaxlesup  11209  xrminmax  11215  summodclem3  11330  zeo3  11814  odd2np1  11819  mod2eq1n2dvds  11825  ndvdsadd  11877  fldivndvdslt  11881  zsupcllemstep  11887  zsupcllemex  11888  zsupssdc  11896  gcdneg  11924  algcvgblem  11990  lcmneg  12015  isprm3  12059  dvdsnprmd  12066  isprm5lem  12082  isprm5  12083  rpexp  12094  pw2dvdslemn  12106  pw2dvdseu  12109  oddpwdclemxy  12110  oddpwdclemdc  12114  oddpwdc  12115  sqpweven  12116  2sqpwodd  12117  sqne2sq  12118  phiprmpw  12163  m1dvdsndvds  12189  pythagtrip  12224  pcgcd1  12268  prmpwdvds  12294  oddennn  12334  ctinfomlemom  12369  ctinfom  12370  isnsgrp  12633  bdxmet  13216  dedekindeulemlu  13314  suplociccex  13318  dedekindicclemlu  13323  efle  13412  logleb  13511  cxple  13552  cxple3  13556  lgsmod  13642  lgsdir2lem2  13645  lgsdir2  13649  lgsne0  13654  lgsprme0  13658  decidi  13751  uzdcinzz  13754  bj-charfunbi  13768  bj-nalset  13852  bj-nnelirr  13910  subctctexmid  13956  nninfsellemeq  13969  ismkvnnlem  14006