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:  stbid  839  dcbid  845  con1biidc  884  pm4.54dc  909  ifpbi123d  1000  xorbi2d  1424  xorbi1d  1425  pm5.18im  1429  pm5.24dc  1442  neeq1  2415  neeq2  2416  necon3abid  2441  neleq1  2501  neleq2  2502  cdeqnot  3019  ru  3030  sbcng  3072  sbcnel12g  3144  sbcne12g  3145  difjust  3201  eldif  3209  dfdif3  3317  difeq2  3319  disjne  3548  eldifpr  3696  eldiftp  3715  prel12  3854  nalset  4219  pwnss  4249  poeq1  4396  pocl  4400  swopo  4403  sotritrieq  4422  tz7.2  4451  regexmidlem1  4631  regexmid  4633  nordeq  4642  nlimsucg  4664  nndceq0  4716  nnregexmid  4719  poinxp  4795  posng  4798  intirr  5123  poirr2  5129  cnvpom  5279  fndmdif  5752  isopolem  5963  canth  5969  poxp  6397  nnmword  6686  brdifun  6729  swoer  6730  2dom  6980  pw2f1odclem  7020  php5  7044  php5dom  7049  findcard2s  7079  fimax2gtrilemstep  7090  fimax2gtri  7091  fidcenumlemrk  7153  supeq3  7189  supeq123d  7190  supmoti  7192  eqsupti  7195  supubti  7198  supsnti  7204  isotilem  7205  isoti  7206  supisolem  7207  supisoex  7208  cnvinfex  7217  cnvti  7218  eqinfti  7219  infvalti  7221  difinfsn  7299  ismkv  7352  ismkvnex  7354  mkvprop  7357  fodjumkvlemres  7358  enmkvlem  7360  onntri35  7455  onntri45  7459  tapeq1  7471  netap  7473  2omotaplemap  7476  exmidapne  7479  pitric  7541  addnidpig  7556  ltsonq  7618  elinp  7694  prltlu  7707  prdisj  7712  ltexprlemdisj  7826  suplocexpr  7945  ltposr  7983  aptisr  7999  suplocsrlem  8028  axpre-ltirr  8102  axpre-apti  8105  axpre-suploclemres  8121  axpre-suploc  8122  xrlenlt  8244  axapti  8250  axsuploc  8252  lttri3  8259  ltne  8264  leadd1  8610  reapti  8759  lemul1  8773  apirr  8785  apti  8802  apcon4bid  8804  lediv1  9049  lemuldiv  9061  lerec  9064  le2msq  9081  suprnubex  9133  suprleubex  9134  avgle1  9385  avgle2  9386  znnnlt1  9527  supinfneg  9829  infsupneg  9830  infregelbex  9832  eluzdc  9844  qapne  9873  xrltne  10048  xleneg  10072  nn0disj  10373  nelfzo  10387  elfzonelfzo  10476  fvinim0ffz  10488  zsupcllemstep  10490  zsupcllemex  10491  zsupssdc  10499  ioo0  10520  ico0  10522  ioc0  10523  flqlt  10544  expeq0  10833  nn0leexp2  10973  leisorel  11102  wrdsymb0  11150  swrdnd  11244  maxleim  11783  maxabslemval  11786  maxleast  11791  minmax  11808  xrmaxleim  11822  xrmaxiflemval  11828  xrmaxlesup  11837  xrminmax  11843  summodclem3  11959  zeo3  12447  odd2np1  12452  mod2eq1n2dvds  12458  ndvdsadd  12510  fldivndvdslt  12516  bitsfval  12521  bitsval  12522  bits0  12527  bitsp1  12530  bitsmod  12535  bitscmp  12537  bitsinv1lem  12540  gcdneg  12571  nninfctlemfo  12629  algcvgblem  12639  lcmneg  12664  isprm3  12708  dvdsnprmd  12715  isprm5lem  12731  isprm5  12732  rpexp  12743  pw2dvdslemn  12755  pw2dvdseu  12758  oddpwdclemxy  12759  oddpwdclemdc  12763  oddpwdc  12764  sqpweven  12765  2sqpwodd  12766  sqne2sq  12767  phiprmpw  12812  m1dvdsndvds  12839  pythagtrip  12874  pcgcd1  12919  prmpwdvds  12946  oddennn  13031  ctinfomlemom  13066  ctinfom  13067  isnsgrp  13507  nzrunit  14221  bdxmet  15244  dedekindeulemlu  15364  suplociccex  15368  dedekindicclemlu  15373  efle  15519  logleb  15618  cxple  15660  cxple3  15664  lgsmod  15774  lgsdir2lem2  15777  lgsdir2  15781  lgsne0  15786  lgsprme0  15790  lgsquadlem1  15825  2lgslem3  15849  2lgsoddprm  15861  vtxd0nedgbfi  16169  1hevtxdg0fi  16177  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  eupth2lem3lem7fi  16344  eupth2lemsfi  16348  eupth2fi  16349  konigsberglem4  16361  decidi  16442  uzdcinzz  16445  bj-charfunbi  16457  bj-nalset  16541  bj-nnelirr  16599  subctctexmid  16652  nninfsellemeq  16667  ismkvnnlem  16708