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	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
notbid	|- ( ph -> ( -. ps <-> -. ch ) )

Proof of Theorem notbid

Step	Hyp	Ref	Expression
1		notbid.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		notbi 672	. 2 |- ( ( ps <-> ch ) -> ( -. ps <-> -. ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( -. ps <-> -. ch ) )

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  11147  swrdnd  11241  maxleim  11767  maxabslemval  11770  maxleast  11775  minmax  11792  xrmaxleim  11806  xrmaxiflemval  11812  xrmaxlesup  11821  xrminmax  11827  summodclem3  11943  zeo3  12431  odd2np1  12436  mod2eq1n2dvds  12442  ndvdsadd  12494  fldivndvdslt  12500  bitsfval  12505  bitsval  12506  bits0  12511  bitsp1  12514  bitsmod  12519  bitscmp  12521  bitsinv1lem  12524  gcdneg  12555  nninfctlemfo  12613  algcvgblem  12623  lcmneg  12648  isprm3  12692  dvdsnprmd  12699  isprm5lem  12715  isprm5  12716  rpexp  12727  pw2dvdslemn  12739  pw2dvdseu  12742  oddpwdclemxy  12743  oddpwdclemdc  12747  oddpwdc  12748  sqpweven  12749  2sqpwodd  12750  sqne2sq  12751  phiprmpw  12796  m1dvdsndvds  12823  pythagtrip  12858  pcgcd1  12903  prmpwdvds  12930  oddennn  13015  ctinfomlemom  13050  ctinfom  13051  isnsgrp  13491  nzrunit  14205  bdxmet  15228  dedekindeulemlu  15348  suplociccex  15352  dedekindicclemlu  15357  efle  15503  logleb  15602  cxple  15644  cxple3  15648  lgsmod  15758  lgsdir2lem2  15761  lgsdir2  15765  lgsne0  15770  lgsprme0  15774  lgsquadlem1  15809  2lgslem3  15833  2lgsoddprm  15845  vtxd0nedgbfi  16153  1hevtxdg0fi  16161  eupth2lem3lem3fi  16324  eupth2lem3lem6fi  16325  eupth2lem3lem4fi  16327  eupth2lem3lem7fi  16328  eupth2lemsfi  16332  eupth2fi  16333  decidi  16412  uzdcinzz  16415  bj-charfunbi  16427  bj-nalset  16511  bj-nnelirr  16569  subctctexmid  16622  nninfsellemeq  16637  ismkvnnlem  16677