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  7249  supeq123d  7250  supmoti  7252  eqsupti  7255  supubti  7258  supsnti  7264  isotilem  7265  isoti  7266  supisolem  7267  supisoex  7268  cnvinfex  7277  cnvti  7278  eqinfti  7279  infvalti  7281  difinfsn  7359  ismkv  7412  ismkvnex  7414  mkvprop  7417  fodjumkvlemres  7418  enmkvlem  7420  onntri35  7515  onntri45  7519  tapeq1  7531  netap  7533  2omotaplemap  7536  exmidapne  7539  pitric  7601  addnidpig  7616  ltsonq  7678  elinp  7754  prltlu  7767  prdisj  7772  ltexprlemdisj  7886  suplocexpr  8005  ltposr  8043  aptisr  8059  suplocsrlem  8088  axpre-ltirr  8162  axpre-apti  8165  axpre-suploclemres  8181  axpre-suploc  8182  xrlenlt  8303  axapti  8309  axsuploc  8311  lttri3  8318  ltne  8323  leadd1  8669  reapti  8818  lemul1  8832  apirr  8844  apti  8861  apcon4bid  8863  lediv1  9108  lemuldiv  9120  lerec  9123  le2msq  9140  suprnubex  9192  suprleubex  9193  avgle1  9444  avgle2  9445  znnnlt1  9588  supinfneg  9890  infsupneg  9891  infregelbex  9893  eluzdc  9905  qapne  9934  xrltne  10109  xleneg  10133  nn0disj  10435  nelfzo  10449  elfzonelfzo  10538  fvinim0ffz  10550  zsupcllemstep  10552  zsupcllemex  10553  zsupssdc  10561  ioo0  10582  ico0  10584  ioc0  10585  flqlt  10606  expeq0  10895  nn0leexp2  11035  leisorel  11164  wrdsymb0  11212  swrdnd  11306  maxleim  11845  maxabslemval  11848  maxleast  11853  minmax  11870  xrmaxleim  11884  xrmaxiflemval  11890  xrmaxlesup  11899  xrminmax  11905  summodclem3  12021  zeo3  12509  odd2np1  12514  mod2eq1n2dvds  12520  ndvdsadd  12572  fldivndvdslt  12578  bitsfval  12583  bitsval  12584  bits0  12589  bitsp1  12592  bitsmod  12597  bitscmp  12599  bitsinv1lem  12602  gcdneg  12633  nninfctlemfo  12691  algcvgblem  12701  lcmneg  12726  isprm3  12770  dvdsnprmd  12777  isprm5lem  12793  isprm5  12794  rpexp  12805  pw2dvdslemn  12817  pw2dvdseu  12820  oddpwdclemxy  12821  oddpwdclemdc  12825  oddpwdc  12826  sqpweven  12827  2sqpwodd  12828  sqne2sq  12829  phiprmpw  12874  m1dvdsndvds  12901  pythagtrip  12936  pcgcd1  12981  prmpwdvds  13008  oddennn  13093  ctinfomlemom  13128  ctinfom  13129  isnsgrp  13569  nzrunit  14283  bdxmet  15312  dedekindeulemlu  15432  suplociccex  15436  dedekindicclemlu  15441  efle  15587  logleb  15686  cxple  15728  cxple3  15732  lgsmod  15845  lgsdir2lem2  15848  lgsdir2  15852  lgsne0  15857  lgsprme0  15861  lgsquadlem1  15896  2lgslem3  15920  2lgsoddprm  15932  vtxd0nedgbfi  16240  1hevtxdg0fi  16248  eupth2lem3lem3fi  16411  eupth2lem3lem6fi  16412  eupth2lem3lem4fi  16414  eupth2lem3lem7fi  16415  eupth2lemsfi  16419  eupth2fi  16420  konigsberglem4  16432  decidi  16513  uzdcinzz  16516  bj-charfunbi  16527  bj-nalset  16611  bj-nnelirr  16669  subctctexmid  16722  exmidnotnotr  16727  exmidcon  16728  nninfsellemeq  16740  ismkvnnlem  16785