Theorem notbid 671

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 670	. 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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  837  dcbid  843  con1biidc  882  pm4.54dc  907  ifpbi123d  998  xorbi2d  1422  xorbi1d  1423  pm5.18im  1427  pm5.24dc  1440  neeq1  2413  neeq2  2414  necon3abid  2439  neleq1  2499  neleq2  2500  cdeqnot  3016  ru  3027  sbcng  3069  sbcnel12g  3141  sbcne12g  3142  difjust  3198  eldif  3206  dfdif3  3314  difeq2  3316  disjne  3545  eldifpr  3693  eldiftp  3712  prel12  3849  nalset  4214  pwnss  4243  poeq1  4390  pocl  4394  swopo  4397  sotritrieq  4416  tz7.2  4445  regexmidlem1  4625  regexmid  4627  nordeq  4636  nlimsucg  4658  nndceq0  4710  nnregexmid  4713  poinxp  4788  posng  4791  intirr  5115  poirr2  5121  cnvpom  5271  fndmdif  5742  isopolem  5952  canth  5958  poxp  6384  nnmword  6672  brdifun  6715  swoer  6716  2dom  6966  pw2f1odclem  7003  php5  7027  php5dom  7032  findcard2s  7060  fimax2gtrilemstep  7071  fimax2gtri  7072  fidcenumlemrk  7132  supeq3  7168  supeq123d  7169  supmoti  7171  eqsupti  7174  supubti  7177  supsnti  7183  isotilem  7184  isoti  7185  supisolem  7186  supisoex  7187  cnvinfex  7196  cnvti  7197  eqinfti  7198  infvalti  7200  difinfsn  7278  ismkv  7331  ismkvnex  7333  mkvprop  7336  fodjumkvlemres  7337  enmkvlem  7339  onntri35  7433  onntri45  7437  tapeq1  7449  netap  7451  2omotaplemap  7454  exmidapne  7457  pitric  7519  addnidpig  7534  ltsonq  7596  elinp  7672  prltlu  7685  prdisj  7690  ltexprlemdisj  7804  suplocexpr  7923  ltposr  7961  aptisr  7977  suplocsrlem  8006  axpre-ltirr  8080  axpre-apti  8083  axpre-suploclemres  8099  axpre-suploc  8100  xrlenlt  8222  axapti  8228  axsuploc  8230  lttri3  8237  ltne  8242  leadd1  8588  reapti  8737  lemul1  8751  apirr  8763  apti  8780  apcon4bid  8782  lediv1  9027  lemuldiv  9039  lerec  9042  le2msq  9059  suprnubex  9111  suprleubex  9112  avgle1  9363  avgle2  9364  znnnlt1  9505  supinfneg  9802  infsupneg  9803  infregelbex  9805  eluzdc  9817  qapne  9846  xrltne  10021  xleneg  10045  nn0disj  10346  nelfzo  10360  elfzonelfzo  10448  fvinim0ffz  10459  zsupcllemstep  10461  zsupcllemex  10462  zsupssdc  10470  ioo0  10491  ico0  10493  ioc0  10494  flqlt  10515  expeq0  10804  nn0leexp2  10944  leisorel  11072  wrdsymb0  11117  swrdnd  11207  maxleim  11732  maxabslemval  11735  maxleast  11740  minmax  11757  xrmaxleim  11771  xrmaxiflemval  11777  xrmaxlesup  11786  xrminmax  11792  summodclem3  11907  zeo3  12395  odd2np1  12400  mod2eq1n2dvds  12406  ndvdsadd  12458  fldivndvdslt  12464  bitsfval  12469  bitsval  12470  bits0  12475  bitsp1  12478  bitsmod  12483  bitscmp  12485  bitsinv1lem  12488  gcdneg  12519  nninfctlemfo  12577  algcvgblem  12587  lcmneg  12612  isprm3  12656  dvdsnprmd  12663  isprm5lem  12679  isprm5  12680  rpexp  12691  pw2dvdslemn  12703  pw2dvdseu  12706  oddpwdclemxy  12707  oddpwdclemdc  12711  oddpwdc  12712  sqpweven  12713  2sqpwodd  12714  sqne2sq  12715  phiprmpw  12760  m1dvdsndvds  12787  pythagtrip  12822  pcgcd1  12867  prmpwdvds  12894  oddennn  12979  ctinfomlemom  13014  ctinfom  13015  isnsgrp  13455  nzrunit  14168  bdxmet  15191  dedekindeulemlu  15311  suplociccex  15315  dedekindicclemlu  15320  efle  15466  logleb  15565  cxple  15607  cxple3  15611  lgsmod  15721  lgsdir2lem2  15724  lgsdir2  15728  lgsne0  15733  lgsprme0  15737  lgsquadlem1  15772  2lgslem3  15796  2lgsoddprm  15808  vtxd0nedgbfi  16059  decidi  16242  uzdcinzz  16245  bj-charfunbi  16257  bj-nalset  16341  bj-nnelirr  16399  subctctexmid  16453  nninfsellemeq  16468  ismkvnnlem  16508