Theorem notbid 656

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 655	. 2 ⊢ ((𝜓 ↔ 𝜒) → (¬ 𝜓 ↔ ¬ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  817  dcbid  823  con1biidc  862  pm4.54dc  887  xorbi2d  1358  xorbi1d  1359  pm5.18im  1363  pm5.24dc  1376  neeq1  2319  neeq2  2320  necon3abid  2345  neleq1  2405  neleq2  2406  cdeqnot  2892  ru  2903  sbcng  2944  sbcnel12g  3014  sbcne12g  3015  difjust  3067  eldif  3075  dfdif3  3181  difeq2  3183  disjne  3411  prel12  3693  nalset  4053  pwnss  4078  poeq1  4216  pocl  4220  swopo  4223  sotritrieq  4242  tz7.2  4271  regexmidlem1  4443  regexmid  4445  nordeq  4454  nlimsucg  4476  nndceq0  4526  nnregexmid  4529  poinxp  4603  posng  4606  intirr  4920  poirr2  4926  cnvpom  5076  fndmdif  5518  isopolem  5716  poxp  6122  nnmword  6407  brdifun  6449  swoer  6450  2dom  6692  php5  6745  php5dom  6750  findcard2s  6777  fimax2gtrilemstep  6787  fimax2gtri  6788  fidcenumlemrk  6835  supeq3  6870  supeq123d  6871  supmoti  6873  eqsupti  6876  supubti  6879  supsnti  6885  isotilem  6886  isoti  6887  supisolem  6888  supisoex  6889  cnvinfex  6898  cnvti  6899  eqinfti  6900  infvalti  6902  difinfsn  6978  ismkv  7020  ismkvnex  7022  mkvprop  7025  fodjumkvlemres  7026  pitric  7122  addnidpig  7137  ltsonq  7199  elinp  7275  prltlu  7288  prdisj  7293  ltexprlemdisj  7407  suplocexpr  7526  ltposr  7564  aptisr  7580  suplocsrlem  7609  axpre-ltirr  7683  axpre-apti  7686  axpre-suploclemres  7702  axpre-suploc  7703  xrlenlt  7822  axapti  7828  axsuploc  7830  lttri3  7837  ltne  7842  leadd1  8185  reapti  8334  lemul1  8348  apirr  8360  apti  8377  apcon4bid  8379  lediv1  8620  lemuldiv  8632  lerec  8635  le2msq  8652  suprnubex  8704  suprleubex  8705  avgle1  8953  avgle2  8954  znnnlt1  9095  supinfneg  9383  infsupneg  9384  eluzdc  9397  qapne  9424  xrltne  9589  xleneg  9613  nn0disj  9908  elfzonelfzo  10000  fvinim0ffz  10011  ioo0  10030  ico0  10032  ioc0  10033  flqlt  10049  expeq0  10317  leisorel  10573  maxleim  10970  maxabslemval  10973  maxleast  10978  minmax  10994  xrmaxleim  11006  xrmaxiflemval  11012  xrmaxlesup  11021  xrminmax  11027  summodclem3  11142  zeo3  11554  odd2np1  11559  mod2eq1n2dvds  11565  ndvdsadd  11617  fldivndvdslt  11621  zsupcllemstep  11627  zsupcllemex  11628  gcdneg  11659  algcvgblem  11719  lcmneg  11744  isprm3  11788  dvdsnprmd  11795  rpexp  11820  pw2dvdslemn  11832  pw2dvdseu  11835  oddpwdclemxy  11836  oddpwdclemdc  11840  oddpwdc  11841  sqpweven  11842  2sqpwodd  11843  sqne2sq  11844  phiprmpw  11887  oddennn  11894  ctinfomlemom  11929  ctinfom  11930  bdxmet  12659  dedekindeulemlu  12757  suplociccex  12761  dedekindicclemlu  12766  decidi  12991  uzdcinzz  12994  bj-nalset  13082  bj-nnelirr  13140  subctctexmid  13185  nninfsellemeq  13199