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  4175  pwnss  4204  poeq1  4347  pocl  4351  swopo  4354  sotritrieq  4373  tz7.2  4402  regexmidlem1  4582  regexmid  4584  nordeq  4593  nlimsucg  4615  nndceq0  4667  nnregexmid  4670  poinxp  4745  posng  4748  intirr  5070  poirr2  5076  cnvpom  5226  fndmdif  5687  isopolem  5893  canth  5899  poxp  6320  nnmword  6606  brdifun  6649  swoer  6650  2dom  6899  pw2f1odclem  6933  php5  6957  php5dom  6962  findcard2s  6989  fimax2gtrilemstep  6999  fimax2gtri  7000  fidcenumlemrk  7058  supeq3  7094  supeq123d  7095  supmoti  7097  eqsupti  7100  supubti  7103  supsnti  7109  isotilem  7110  isoti  7111  supisolem  7112  supisoex  7113  cnvinfex  7122  cnvti  7123  eqinfti  7124  infvalti  7126  difinfsn  7204  ismkv  7257  ismkvnex  7259  mkvprop  7262  fodjumkvlemres  7263  enmkvlem  7265  onntri35  7351  onntri45  7355  tapeq1  7366  netap  7368  2omotaplemap  7371  exmidapne  7374  pitric  7436  addnidpig  7451  ltsonq  7513  elinp  7589  prltlu  7602  prdisj  7607  ltexprlemdisj  7721  suplocexpr  7840  ltposr  7878  aptisr  7894  suplocsrlem  7923  axpre-ltirr  7997  axpre-apti  8000  axpre-suploclemres  8016  axpre-suploc  8017  xrlenlt  8139  axapti  8145  axsuploc  8147  lttri3  8154  ltne  8159  leadd1  8505  reapti  8654  lemul1  8668  apirr  8680  apti  8697  apcon4bid  8699  lediv1  8944  lemuldiv  8956  lerec  8959  le2msq  8976  suprnubex  9028  suprleubex  9029  avgle1  9280  avgle2  9281  znnnlt1  9422  supinfneg  9718  infsupneg  9719  infregelbex  9721  eluzdc  9733  qapne  9762  xrltne  9937  xleneg  9961  nn0disj  10262  nelfzo  10276  elfzonelfzo  10361  fvinim0ffz  10372  zsupcllemstep  10374  zsupcllemex  10375  zsupssdc  10383  ioo0  10404  ico0  10406  ioc0  10407  flqlt  10428  expeq0  10717  nn0leexp2  10857  leisorel  10984  wrdsymb0  11028  swrdnd  11115  maxleim  11549  maxabslemval  11552  maxleast  11557  minmax  11574  xrmaxleim  11588  xrmaxiflemval  11594  xrmaxlesup  11603  xrminmax  11609  summodclem3  11724  zeo3  12212  odd2np1  12217  mod2eq1n2dvds  12223  ndvdsadd  12275  fldivndvdslt  12281  bitsfval  12286  bitsval  12287  bits0  12292  bitsp1  12295  bitsmod  12300  bitscmp  12302  bitsinv1lem  12305  gcdneg  12336  nninfctlemfo  12394  algcvgblem  12404  lcmneg  12429  isprm3  12473  dvdsnprmd  12480  isprm5lem  12496  isprm5  12497  rpexp  12508  pw2dvdslemn  12520  pw2dvdseu  12523  oddpwdclemxy  12524  oddpwdclemdc  12528  oddpwdc  12529  sqpweven  12530  2sqpwodd  12531  sqne2sq  12532  phiprmpw  12577  m1dvdsndvds  12604  pythagtrip  12639  pcgcd1  12684  prmpwdvds  12711  oddennn  12796  ctinfomlemom  12831  ctinfom  12832  isnsgrp  13271  nzrunit  13983  bdxmet  15006  dedekindeulemlu  15126  suplociccex  15130  dedekindicclemlu  15135  efle  15281  logleb  15380  cxple  15422  cxple3  15426  lgsmod  15536  lgsdir2lem2  15539  lgsdir2  15543  lgsne0  15548  lgsprme0  15552  lgsquadlem1  15587  2lgslem3  15611  2lgsoddprm  15623  decidi  15768  uzdcinzz  15771  bj-charfunbi  15784  bj-nalset  15868  bj-nnelirr  15926  subctctexmid  15974  nninfsellemeq  15988  ismkvnnlem  16028