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  2416  neeq2  2417  necon3abid  2442  neleq1  2502  neleq2  2503  cdeqnot  3020  ru  3031  sbcng  3073  sbcnel12g  3145  sbcne12g  3146  difjust  3202  eldif  3210  dfdif3  3319  difeq2  3321  disjne  3550  eldifpr  3700  eldiftp  3719  prel12  3859  nalset  4224  pwnss  4255  poeq1  4402  pocl  4406  swopo  4409  sotritrieq  4428  tz7.2  4457  regexmidlem1  4637  regexmid  4639  nordeq  4648  nlimsucg  4670  nndceq0  4722  nnregexmid  4725  poinxp  4801  posng  4804  intirr  5130  poirr2  5136  cnvpom  5286  fndmdif  5761  isopolem  5973  canth  5979  poxp  6406  nnmword  6729  brdifun  6772  swoer  6773  2dom  7023  pw2f1odclem  7063  php5  7087  php5dom  7092  findcard2s  7122  fimax2gtrilemstep  7133  fimax2gtri  7134  fidcenumlemrk  7196  supeq3  7232  supeq123d  7233  supmoti  7235  eqsupti  7238  supubti  7241  supsnti  7247  isotilem  7248  isoti  7249  supisolem  7250  supisoex  7251  cnvinfex  7260  cnvti  7261  eqinfti  7262  infvalti  7264  difinfsn  7342  ismkv  7395  ismkvnex  7397  mkvprop  7400  fodjumkvlemres  7401  enmkvlem  7403  onntri35  7498  onntri45  7502  tapeq1  7514  netap  7516  2omotaplemap  7519  exmidapne  7522  pitric  7584  addnidpig  7599  ltsonq  7661  elinp  7737  prltlu  7750  prdisj  7755  ltexprlemdisj  7869  suplocexpr  7988  ltposr  8026  aptisr  8042  suplocsrlem  8071  axpre-ltirr  8145  axpre-apti  8148  axpre-suploclemres  8164  axpre-suploc  8165  xrlenlt  8286  axapti  8292  axsuploc  8294  lttri3  8301  ltne  8306  leadd1  8652  reapti  8801  lemul1  8815  apirr  8827  apti  8844  apcon4bid  8846  lediv1  9091  lemuldiv  9103  lerec  9106  le2msq  9123  suprnubex  9175  suprleubex  9176  avgle1  9427  avgle2  9428  znnnlt1  9571  supinfneg  9873  infsupneg  9874  infregelbex  9876  eluzdc  9888  qapne  9917  xrltne  10092  xleneg  10116  nn0disj  10418  nelfzo  10432  elfzonelfzo  10521  fvinim0ffz  10533  zsupcllemstep  10535  zsupcllemex  10536  zsupssdc  10544  ioo0  10565  ico0  10567  ioc0  10568  flqlt  10589  expeq0  10878  nn0leexp2  11018  leisorel  11147  wrdsymb0  11195  swrdnd  11289  maxleim  11828  maxabslemval  11831  maxleast  11836  minmax  11853  xrmaxleim  11867  xrmaxiflemval  11873  xrmaxlesup  11882  xrminmax  11888  summodclem3  12004  zeo3  12492  odd2np1  12497  mod2eq1n2dvds  12503  ndvdsadd  12555  fldivndvdslt  12561  bitsfval  12566  bitsval  12567  bits0  12572  bitsp1  12575  bitsmod  12580  bitscmp  12582  bitsinv1lem  12585  gcdneg  12616  nninfctlemfo  12674  algcvgblem  12684  lcmneg  12709  isprm3  12753  dvdsnprmd  12760  isprm5lem  12776  isprm5  12777  rpexp  12788  pw2dvdslemn  12800  pw2dvdseu  12803  oddpwdclemxy  12804  oddpwdclemdc  12808  oddpwdc  12809  sqpweven  12810  2sqpwodd  12811  sqne2sq  12812  phiprmpw  12857  m1dvdsndvds  12884  pythagtrip  12919  pcgcd1  12964  prmpwdvds  12991  oddennn  13076  ctinfomlemom  13111  ctinfom  13112  isnsgrp  13552  nzrunit  14266  bdxmet  15295  dedekindeulemlu  15415  suplociccex  15419  dedekindicclemlu  15424  efle  15570  logleb  15669  cxple  15711  cxple3  15715  lgsmod  15828  lgsdir2lem2  15831  lgsdir2  15835  lgsne0  15840  lgsprme0  15844  lgsquadlem1  15879  2lgslem3  15903  2lgsoddprm  15915  vtxd0nedgbfi  16223  1hevtxdg0fi  16231  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  eupth2lem3lem7fi  16398  eupth2lemsfi  16402  eupth2fi  16403  konigsberglem4  16415  decidi  16496  uzdcinzz  16499  bj-charfunbi  16510  bj-nalset  16594  bj-nnelirr  16652  subctctexmid  16705  exmidnotnotr  16710  exmidcon  16711  nninfsellemeq  16723  ismkvnnlem  16768