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  7330  supeq123d  7331  supmoti  7333  eqsupti  7336  supubti  7339  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  cnvinfex  7358  cnvti  7359  eqinfti  7360  infvalti  7362  difinfsn  7440  ismkv  7493  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  onntri35  7596  onntri45  7600  papeq1  7609  papirr  7611  tapeq1  7618  netap  7620  2omotaplemap  7623  exmidapne  7626  pitric  7688  addnidpig  7703  ltsonq  7765  elinp  7841  prltlu  7854  prdisj  7859  ltexprlemdisj  7973  suplocexpr  8092  ltposr  8130  aptisr  8146  suplocsrlem  8175  axpre-ltirr  8249  axpre-apti  8252  axpre-suploclemres  8268  axpre-suploc  8269  xrlenlt  8390  axapti  8396  axsuploc  8398  lttri3  8405  ltne  8410  leadd1  8759  reapti  8909  lemul1  8923  apirr  8935  apti  8952  apcon4bid  8954  lediv1  9201  lemuldiv  9213  lerec  9216  le2msq  9233  suprnubex  9285  suprleubex  9286  avgle1  9550  avgle2  9551  znnnlt1  9696  supinfneg  10004  infsupneg  10005  infregelbex  10007  eluzdc  10019  qapne  10048  xrltne  10225  xleneg  10249  nn0disj  10555  nelfzo  10569  elfzonelfzo  10658  fvinim0ffz  10670  zsupcllemstep  10672  zsupcllemex  10673  zsupssdc  10683  ioo0  10704  ico0  10706  ioc0  10707  flqlt  10731  expeq0  11020  nn0leexp2  11162  hashfibc  11297  leisorel  11303  wrdsymb0  11351  swrdnd  11445  maxleim  11986  maxabslemval  11989  maxleast  11994  minmax  12011  xrmaxleim  12026  xrmaxiflemval  12032  xrmaxlesup  12041  xrminmax  12047  summodclem3  12163  zeo3  12651  odd2np1  12656  mod2eq1n2dvds  12662  ndvdsadd  12714  fldivndvdslt  12720  bitsfval  12725  bitsval  12726  bits0  12731  bitsp1  12734  bitsmod  12739  bitscmp  12741  bitsinv1lem  12744  gcdneg  12775  nninfctlemfo  12833  algcvgblem  12843  lcmneg  12868  isprm3  12912  dvdsnprmd  12919  isprm5lem  12936  isprm5  12937  rpexp  12948  pwbdvdslemn  12960  pwbdvdseu  12963  nnmaxpwlemxy  12964  nnmaxpwlemparts  12968  nnmaxpw  12969  sqpweven  12971  2sqpwodd  12972  sqne2sq  12973  phiprmpw  13020  m1dvdsndvds  13047  pythagtrip  13082  pcgcd1  13127  prmpwdvds  13154  prmlem0  13240  prmlem1a  13241  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemodife  13289  ballotfilem4  13290  ballotfilem7  13328  oddennn  13332  ctinfomlemom  13367  ctinfom  13368  isnsgrp  13770  nzrunit  14544  opprdrng  14669  bdxmet  15651  dedekindeulemlu  15771  suplociccex  15775  dedekindicclemlu  15780  efle  15926  logleb  16027  logdivle  16047  cxple  16072  cxple3  16076  zprmlogbaplem3  16136  zprmlogbap  16137  bposlem1  16209  lgsmod  16243  lgsdir2lem2  16246  lgsdir2  16250  lgsne0  16255  lgsprme0  16259  lgsquadlem1  16294  2lgslem3  16318  2lgsoddprm  16330  vtxd0nedgbfi  16638  1hevtxdg0fi  16646  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  eupth2lemsfi  16817  eupth2fi  16818  konigsberglem4  16830  decidi  16921  uzdcinzz  16924  bj-charfunbi  16935  bj-nalset  17019  bj-nnelirr  17077  subctctexmid  17128  exmidnotnotr  17134  exmidcon  17135  stnot  17137  wexmiddc  17140  nninfsellemeq  17155  ismkvnnlem  17200