Theorem notbid 668

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 667	. 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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  833  dcbid  839  con1biidc  878  pm4.54dc  903  xorbi2d  1391  xorbi1d  1392  pm5.18im  1396  pm5.24dc  1409  neeq1  2380  neeq2  2381  necon3abid  2406  neleq1  2466  neleq2  2467  cdeqnot  2977  ru  2988  sbcng  3030  sbcnel12g  3101  sbcne12g  3102  difjust  3158  eldif  3166  dfdif3  3274  difeq2  3276  disjne  3505  eldifpr  3650  eldiftp  3669  prel12  3802  nalset  4164  pwnss  4193  poeq1  4335  pocl  4339  swopo  4342  sotritrieq  4361  tz7.2  4390  regexmidlem1  4570  regexmid  4572  nordeq  4581  nlimsucg  4603  nndceq0  4655  nnregexmid  4658  poinxp  4733  posng  4736  intirr  5057  poirr2  5063  cnvpom  5213  fndmdif  5670  isopolem  5872  canth  5878  poxp  6299  nnmword  6585  brdifun  6628  swoer  6629  2dom  6873  pw2f1odclem  6904  php5  6928  php5dom  6933  findcard2s  6960  fimax2gtrilemstep  6970  fimax2gtri  6971  fidcenumlemrk  7029  supeq3  7065  supeq123d  7066  supmoti  7068  eqsupti  7071  supubti  7074  supsnti  7080  isotilem  7081  isoti  7082  supisolem  7083  supisoex  7084  cnvinfex  7093  cnvti  7094  eqinfti  7095  infvalti  7097  difinfsn  7175  ismkv  7228  ismkvnex  7230  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  onntri35  7320  onntri45  7324  tapeq1  7335  netap  7337  2omotaplemap  7340  exmidapne  7343  pitric  7405  addnidpig  7420  ltsonq  7482  elinp  7558  prltlu  7571  prdisj  7576  ltexprlemdisj  7690  suplocexpr  7809  ltposr  7847  aptisr  7863  suplocsrlem  7892  axpre-ltirr  7966  axpre-apti  7969  axpre-suploclemres  7985  axpre-suploc  7986  xrlenlt  8108  axapti  8114  axsuploc  8116  lttri3  8123  ltne  8128  leadd1  8474  reapti  8623  lemul1  8637  apirr  8649  apti  8666  apcon4bid  8668  lediv1  8913  lemuldiv  8925  lerec  8928  le2msq  8945  suprnubex  8997  suprleubex  8998  avgle1  9249  avgle2  9250  znnnlt1  9391  supinfneg  9686  infsupneg  9687  infregelbex  9689  eluzdc  9701  qapne  9730  xrltne  9905  xleneg  9929  nn0disj  10230  nelfzo  10244  elfzonelfzo  10323  fvinim0ffz  10334  zsupcllemstep  10336  zsupcllemex  10337  zsupssdc  10345  ioo0  10366  ico0  10368  ioc0  10369  flqlt  10390  expeq0  10679  nn0leexp2  10819  leisorel  10946  wrdsymb0  10984  maxleim  11387  maxabslemval  11390  maxleast  11395  minmax  11412  xrmaxleim  11426  xrmaxiflemval  11432  xrmaxlesup  11441  xrminmax  11447  summodclem3  11562  zeo3  12050  odd2np1  12055  mod2eq1n2dvds  12061  ndvdsadd  12113  fldivndvdslt  12119  bitsfval  12124  bitsval  12125  bits0  12130  bitsp1  12133  bitsmod  12138  bitscmp  12140  bitsinv1lem  12143  gcdneg  12174  nninfctlemfo  12232  algcvgblem  12242  lcmneg  12267  isprm3  12311  dvdsnprmd  12318  isprm5lem  12334  isprm5  12335  rpexp  12346  pw2dvdslemn  12358  pw2dvdseu  12361  oddpwdclemxy  12362  oddpwdclemdc  12366  oddpwdc  12367  sqpweven  12368  2sqpwodd  12369  sqne2sq  12370  phiprmpw  12415  m1dvdsndvds  12442  pythagtrip  12477  pcgcd1  12522  prmpwdvds  12549  oddennn  12634  ctinfomlemom  12669  ctinfom  12670  isnsgrp  13108  nzrunit  13820  bdxmet  14821  dedekindeulemlu  14941  suplociccex  14945  dedekindicclemlu  14950  efle  15096  logleb  15195  cxple  15237  cxple3  15241  lgsmod  15351  lgsdir2lem2  15354  lgsdir2  15358  lgsne0  15363  lgsprme0  15367  lgsquadlem1  15402  2lgslem3  15426  2lgsoddprm  15438  decidi  15525  uzdcinzz  15528  bj-charfunbi  15541  bj-nalset  15625  bj-nnelirr  15683  subctctexmid  15731  nninfsellemeq  15745  ismkvnnlem  15783