Theorem notbid 673

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 672	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  annotanannot  676  stbid  840  dcbid  846  con1biidc  885  pm4.54dc  910  ifpbi123d  1001  xorbi2d  1425  xorbi1d  1426  pm5.18im  1430  pm5.24dc  1443  neeq1  2425  neeq2  2426  necon3abid  2451  neleq1  2511  neleq2  2512  cdeqnot  3030  ru  3041  sbcng  3083  sbcnel12g  3155  sbcne12g  3156  difjust  3212  eldif  3220  dfdif3  3329  difeq2  3331  disjne  3562  eldifpr  3716  eldiftp  3735  prel12  3875  nalset  4240  pwnss  4272  poeq1  4420  pocl  4424  swopo  4427  sotritrieq  4446  tz7.2  4475  regexmidlem1  4655  regexmid  4657  nordeq  4666  nlimsucg  4688  nndceq0  4740  nnregexmid  4743  poinxp  4819  posng  4822  intirr  5149  poirr2  5155  cnvpom  5305  fndmdif  5783  isopolem  5995  canth  6001  poxp  6428  nnmword  6751  brdifun  6794  swoer  6795  2dom  7046  pw2f1odclem  7087  php5  7112  php5dom  7117  findcard2s  7147  fimax2gtrilemstep  7158  fimax2gtri  7159  fidcenumlemrk  7224  supeq3  7281  supeq123d  7282  supmoti  7284  eqsupti  7287  supubti  7290  supsnti  7296  isotilem  7297  isoti  7298  supisolem  7299  supisoex  7300  cnvinfex  7309  cnvti  7310  eqinfti  7311  infvalti  7313  difinfsn  7391  ismkv  7444  ismkvnex  7446  mkvprop  7449  fodjumkvlemres  7450  enmkvlem  7452  onntri35  7547  onntri45  7551  papirr  7560  tapeq1  7566  netap  7568  2omotaplemap  7571  exmidapne  7574  pitric  7636  addnidpig  7651  ltsonq  7713  elinp  7789  prltlu  7802  prdisj  7807  ltexprlemdisj  7921  suplocexpr  8040  ltposr  8078  aptisr  8094  suplocsrlem  8123  axpre-ltirr  8197  axpre-apti  8200  axpre-suploclemres  8216  axpre-suploc  8217  xrlenlt  8338  axapti  8344  axsuploc  8346  lttri3  8353  ltne  8358  leadd1  8704  reapti  8853  lemul1  8867  apirr  8879  apti  8896  apcon4bid  8898  lediv1  9143  lemuldiv  9155  lerec  9158  le2msq  9175  suprnubex  9227  suprleubex  9228  avgle1  9479  avgle2  9480  znnnlt1  9625  supinfneg  9927  infsupneg  9928  infregelbex  9930  eluzdc  9942  qapne  9971  xrltne  10146  xleneg  10170  nn0disj  10472  nelfzo  10486  elfzonelfzo  10575  fvinim0ffz  10587  zsupcllemstep  10589  zsupcllemex  10590  zsupssdc  10598  ioo0  10619  ico0  10621  ioc0  10622  flqlt  10643  expeq0  10932  nn0leexp2  11072  hashfibc  11207  leisorel  11209  wrdsymb0  11257  swrdnd  11351  maxleim  11890  maxabslemval  11893  maxleast  11898  minmax  11915  xrmaxleim  11929  xrmaxiflemval  11935  xrmaxlesup  11944  xrminmax  11950  summodclem3  12066  zeo3  12554  odd2np1  12559  mod2eq1n2dvds  12565  ndvdsadd  12617  fldivndvdslt  12623  bitsfval  12628  bitsval  12629  bits0  12634  bitsp1  12637  bitsmod  12642  bitscmp  12644  bitsinv1lem  12647  gcdneg  12678  nninfctlemfo  12736  algcvgblem  12746  lcmneg  12771  isprm3  12815  dvdsnprmd  12822  isprm5lem  12838  isprm5  12839  rpexp  12850  pw2dvdslemn  12862  pw2dvdseu  12865  oddpwdclemxy  12866  oddpwdclemdc  12870  oddpwdc  12871  sqpweven  12872  2sqpwodd  12873  sqne2sq  12874  phiprmpw  12919  m1dvdsndvds  12946  pythagtrip  12981  pcgcd1  13026  prmpwdvds  13053  ballotfilem2  13142  oddennn  13143  ctinfomlemom  13178  ctinfom  13179  isnsgrp  13619  nzrunit  14333  bdxmet  15366  dedekindeulemlu  15486  suplociccex  15490  dedekindicclemlu  15495  efle  15641  logleb  15740  cxple  15782  cxple3  15786  lgsmod  15899  lgsdir2lem2  15902  lgsdir2  15906  lgsne0  15911  lgsprme0  15915  lgsquadlem1  15950  2lgslem3  15974  2lgsoddprm  15986  vtxd0nedgbfi  16294  1hevtxdg0fi  16302  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupth2lem3lem7fi  16469  eupth2lemsfi  16473  eupth2fi  16474  konigsberglem4  16486  decidi  16567  uzdcinzz  16570  bj-charfunbi  16581  bj-nalset  16665  bj-nnelirr  16723  subctctexmid  16774  exmidnotnotr  16779  exmidcon  16780  nninfsellemeq  16792  ismkvnnlem  16837