Theorem notbid 677

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 676	. 2 |- ( ( ps <-> ch ) -> ( -. ps <-> -. ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( -. ps <-> -. ch ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  annotanannot  680  stbid  844  dcbid  850  con1biidc  889  pm4.54dc  914  ifpbi123d  1005  xorbi2d  1429  xorbi1d  1430  pm5.18im  1434  pm5.24dc  1447  neeq1  2433  neeq2  2434  necon3abid  2459  neleq1  2519  neleq2  2520  cdeqnot  3039  ru  3050  sbcng  3092  sbcnel12g  3164  sbcne12g  3165  difjust  3221  eldif  3229  dfdif3  3339  difeq2  3341  disjne  3578  ifeqeqxdc  3687  eldifpr  3736  eldiftp  3755  prel12  3896  nalset  4263  pwnss  4296  poeq1  4444  pocl  4448  swopo  4451  sotritrieq  4470  tz7.2  4499  regexmidlem1  4680  regexmid  4682  nordeq  4691  nlimsucg  4713  nndceq0  4765  nnregexmid  4768  poinxp  4844  posng  4847  intirr  5174  poirr2  5180  cnvpom  5330  fndmdif  5814  isopolem  6028  canth  6036  poxp  6468  nnmword  6791  brdifun  6834  swoer  6835  2dom  7093  pw2f1odclem  7134  php5  7159  php5dom  7164  findcard2s  7194  fimax2gtrilemstep  7205  fimax2gtri  7206  fidcenumlemrk  7271  supeq3  7330  supeq123d  7331  supmoti  7333  eqsupti  7336  supubti  7339  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  cnvinfex  7358  cnvti  7359  eqinfti  7360  infvalti  7362  difinfsn  7440  ismkv  7493  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  onntri35  7596  onntri45  7600  papeq1  7609  papirr  7611  tapeq1  7618  netap  7620  2omotaplemap  7623  exmidapne  7626  pitric  7688  addnidpig  7703  ltsonq  7765  elinp  7841  prltlu  7854  prdisj  7859  ltexprlemdisj  7973  suplocexpr  8092  ltposr  8130  aptisr  8146  suplocsrlem  8175  axpre-ltirr  8249  axpre-apti  8252  axpre-suploclemres  8268  axpre-suploc  8269  xrlenlt  8390  axapti  8396  axsuploc  8398  lttri3  8405  ltne  8410  leadd1  8758  reapti  8907  lemul1  8921  apirr  8933  apti  8950  apcon4bid  8952  lediv1  9199  lemuldiv  9211  lerec  9214  le2msq  9231  suprnubex  9283  suprleubex  9284  avgle1  9546  avgle2  9547  znnnlt1  9692  supinfneg  9995  infsupneg  9996  infregelbex  9998  eluzdc  10010  qapne  10039  xrltne  10215  xleneg  10239  nn0disj  10545  nelfzo  10559  elfzonelfzo  10648  fvinim0ffz  10660  zsupcllemstep  10662  zsupcllemex  10663  zsupssdc  10673  ioo0  10694  ico0  10696  ioc0  10697  flqlt  10718  expeq0  11007  nn0leexp2  11148  hashfibc  11283  leisorel  11289  wrdsymb0  11337  swrdnd  11431  maxleim  11971  maxabslemval  11974  maxleast  11979  minmax  11996  xrmaxleim  12010  xrmaxiflemval  12016  xrmaxlesup  12025  xrminmax  12031  summodclem3  12147  zeo3  12635  odd2np1  12640  mod2eq1n2dvds  12646  ndvdsadd  12698  fldivndvdslt  12704  bitsfval  12709  bitsval  12710  bits0  12715  bitsp1  12718  bitsmod  12723  bitscmp  12725  bitsinv1lem  12728  gcdneg  12759  nninfctlemfo  12817  algcvgblem  12827  lcmneg  12852  isprm3  12896  dvdsnprmd  12903  isprm5lem  12919  isprm5  12920  rpexp  12931  pw2dvdslemn  12943  pw2dvdseu  12946  oddpwdclemxy  12947  oddpwdclemdc  12951  oddpwdc  12952  sqpweven  12953  2sqpwodd  12954  sqne2sq  12955  phiprmpw  13000  m1dvdsndvds  13027  pythagtrip  13062  pcgcd1  13107  prmpwdvds  13134  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemodife  13240  ballotfilem4  13241  ballotfilem7  13279  oddennn  13283  ctinfomlemom  13318  ctinfom  13319  isnsgrp  13721  nzrunit  14495  opprdrng  14620  bdxmet  15602  dedekindeulemlu  15722  suplociccex  15726  dedekindicclemlu  15731  efle  15877  logleb  15976  cxple  16019  cxple3  16023  lgsmod  16145  lgsdir2lem2  16148  lgsdir2  16152  lgsne0  16157  lgsprme0  16161  lgsquadlem1  16196  2lgslem3  16220  2lgsoddprm  16232  vtxd0nedgbfi  16540  1hevtxdg0fi  16548  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  eupth2lemsfi  16719  eupth2fi  16720  konigsberglem4  16732  decidi  16823  uzdcinzz  16826  bj-charfunbi  16837  bj-nalset  16921  bj-nnelirr  16979  subctctexmid  17030  exmidnotnotr  17036  exmidcon  17037  stnot  17039  wexmiddc  17042  nninfsellemeq  17057  ismkvnnlem  17102