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  4263  pwnss  4296  poeq1  4444  pocl  4448  swopo  4451  sotritrieq  4470  tz7.2  4499  regexmidlem1  4680  regexmid  4682  nordeq  4691  nlimsucg  4713  nndceq0  4765  nnregexmid  4768  poinxp  4844  posng  4847  intirr  5174  poirr2  5180  cnvpom  5330  fndmdif  5814  isopolem  6028  canth  6036  poxp  6468  nnmword  6791  brdifun  6834  swoer  6835  2dom  7093  pw2f1odclem  7134  php5  7159  php5dom  7164  findcard2s  7194  fimax2gtrilemstep  7205  fimax2gtri  7206  fidcenumlemrk  7271  supeq3  7331  supeq123d  7332  supmoti  7334  eqsupti  7337  supubti  7340  supsnti  7346  isotilem  7347  isoti  7348  supisolem  7349  supisoex  7350  cnvinfex  7359  cnvti  7360  eqinfti  7361  infvalti  7363  difinfsn  7441  ismkv  7494  ismkvnex  7496  mkvprop  7499  fodjumkvlemres  7500  enmkvlem  7502  onntri35  7597  onntri45  7601  papeq1  7610  papirr  7612  tapeq1  7619  netap  7621  2omotaplemap  7624  exmidapne  7627  pitric  7689  addnidpig  7704  ltsonq  7766  elinp  7842  prltlu  7855  prdisj  7860  ltexprlemdisj  7974  suplocexpr  8093  ltposr  8131  aptisr  8147  suplocsrlem  8176  axpre-ltirr  8250  axpre-apti  8253  axpre-suploclemres  8269  axpre-suploc  8270  xrlenlt  8391  axapti  8397  axsuploc  8399  lttri3  8406  ltne  8411  leadd1  8760  reapti  8910  lemul1  8924  apirr  8936  apti  8953  apcon4bid  8955  lediv1  9202  lemuldiv  9214  lerec  9217  le2msq  9234  suprnubex  9286  suprleubex  9287  avgle1  9551  avgle2  9552  znnnlt1  9697  supinfneg  10005  infsupneg  10006  infregelbex  10008  eluzdc  10020  qapne  10049  xrltne  10226  xleneg  10250  nn0disj  10556  nelfzo  10570  elfzonelfzo  10659  fvinim0ffz  10671  zsupcllemstep  10673  zsupcllemex  10674  zsupssdc  10684  ioo0  10705  ico0  10707  ioc0  10708  flqlt  10732  expeq0  11022  nn0leexp2  11164  hashfibc  11299  leisorel  11305  wrdsymb0  11353  swrdnd  11447  maxleim  11988  maxabslemval  11991  maxleast  11996  minmax  12014  xrmaxleim  12029  xrmaxiflemval  12035  xrmaxlesup  12044  xrminmax  12050  summodclem3  12166  zeo3  12654  odd2np1  12659  mod2eq1n2dvds  12665  ndvdsadd  12717  fldivndvdslt  12723  bitsfval  12728  bitsval  12729  bits0  12734  bitsp1  12737  bitsmod  12742  bitscmp  12744  bitsinv1lem  12747  gcdneg  12778  nninfctlemfo  12836  algcvgblem  12846  lcmneg  12871  isprm3  12915  dvdsnprmd  12922  isprm5lem  12939  isprm5  12940  rpexp  12951  pwbdvdslemn  12963  pwbdvdseu  12966  nnmaxpwlemxy  12967  nnmaxpwlemparts  12971  nnmaxpw  12972  sqpweven  12974  2sqpwodd  12975  sqne2sq  12976  phiprmpw  13023  m1dvdsndvds  13050  pythagtrip  13085  pcgcd1  13130  prmpwdvds  13157  prmlem0  13243  prmlem1a  13244  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemodife  13292  ballotfilem4  13293  ballotfilem7  13331  oddennn  13335  ctinfomlemom  13370  ctinfom  13371  isnsgrp  13774  nzrunit  14579  opprdrng  14704  bdxmet  15693  dedekindeulemlu  15813  suplociccex  15817  dedekindicclemlu  15822  efle  15968  logleb  16069  logdivle  16089  cxple  16114  cxple3  16118  zprmlogbaplem3  16178  zprmlogbap  16179  bposlem1  16272  lgsmod  16311  lgsdir2lem2  16314  lgsdir2  16318  lgsne0  16323  lgsprme0  16327  lgsquadlem1  16362  2lgslem3  16386  2lgsoddprm  16398  vtxd0nedgbfi  16706  1hevtxdg0fi  16714  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  eupth2lemsfi  16885  eupth2fi  16886  konigsberglem4  16898  decidi  16989  uzdcinzz  16992  bj-charfunbi  17003  bj-nalset  17087  bj-nnelirr  17145  subctctexmid  17196  exmidnotnotr  17202  exmidcon  17203  stnot  17205  wexmiddc  17208  nninfsellemeq  17223  ismkvnnlem  17269