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	|- ( 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 670	. 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 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  5740  isopolem  5946  canth  5952  poxp  6378  nnmword  6664  brdifun  6707  swoer  6708  2dom  6958  pw2f1odclem  6995  php5  7019  php5dom  7024  findcard2s  7052  fimax2gtrilemstep  7062  fimax2gtri  7063  fidcenumlemrk  7121  supeq3  7157  supeq123d  7158  supmoti  7160  eqsupti  7163  supubti  7166  supsnti  7172  isotilem  7173  isoti  7174  supisolem  7175  supisoex  7176  cnvinfex  7185  cnvti  7186  eqinfti  7187  infvalti  7189  difinfsn  7267  ismkv  7320  ismkvnex  7322  mkvprop  7325  fodjumkvlemres  7326  enmkvlem  7328  onntri35  7422  onntri45  7426  tapeq1  7438  netap  7440  2omotaplemap  7443  exmidapne  7446  pitric  7508  addnidpig  7523  ltsonq  7585  elinp  7661  prltlu  7674  prdisj  7679  ltexprlemdisj  7793  suplocexpr  7912  ltposr  7950  aptisr  7966  suplocsrlem  7995  axpre-ltirr  8069  axpre-apti  8072  axpre-suploclemres  8088  axpre-suploc  8089  xrlenlt  8211  axapti  8217  axsuploc  8219  lttri3  8226  ltne  8231  leadd1  8577  reapti  8726  lemul1  8740  apirr  8752  apti  8769  apcon4bid  8771  lediv1  9016  lemuldiv  9028  lerec  9031  le2msq  9048  suprnubex  9100  suprleubex  9101  avgle1  9352  avgle2  9353  znnnlt1  9494  supinfneg  9790  infsupneg  9791  infregelbex  9793  eluzdc  9805  qapne  9834  xrltne  10009  xleneg  10033  nn0disj  10334  nelfzo  10348  elfzonelfzo  10436  fvinim0ffz  10447  zsupcllemstep  10449  zsupcllemex  10450  zsupssdc  10458  ioo0  10479  ico0  10481  ioc0  10482  flqlt  10503  expeq0  10792  nn0leexp2  10932  leisorel  11059  wrdsymb0  11104  swrdnd  11191  maxleim  11716  maxabslemval  11719  maxleast  11724  minmax  11741  xrmaxleim  11755  xrmaxiflemval  11761  xrmaxlesup  11770  xrminmax  11776  summodclem3  11891  zeo3  12379  odd2np1  12384  mod2eq1n2dvds  12390  ndvdsadd  12442  fldivndvdslt  12448  bitsfval  12453  bitsval  12454  bits0  12459  bitsp1  12462  bitsmod  12467  bitscmp  12469  bitsinv1lem  12472  gcdneg  12503  nninfctlemfo  12561  algcvgblem  12571  lcmneg  12596  isprm3  12640  dvdsnprmd  12647  isprm5lem  12663  isprm5  12664  rpexp  12675  pw2dvdslemn  12687  pw2dvdseu  12690  oddpwdclemxy  12691  oddpwdclemdc  12695  oddpwdc  12696  sqpweven  12697  2sqpwodd  12698  sqne2sq  12699  phiprmpw  12744  m1dvdsndvds  12771  pythagtrip  12806  pcgcd1  12851  prmpwdvds  12878  oddennn  12963  ctinfomlemom  12998  ctinfom  12999  isnsgrp  13439  nzrunit  14152  bdxmet  15175  dedekindeulemlu  15295  suplociccex  15299  dedekindicclemlu  15304  efle  15450  logleb  15549  cxple  15591  cxple3  15595  lgsmod  15705  lgsdir2lem2  15708  lgsdir2  15712  lgsne0  15717  lgsprme0  15721  lgsquadlem1  15756  2lgslem3  15780  2lgsoddprm  15792  decidi  16159  uzdcinzz  16162  bj-charfunbi  16174  bj-nalset  16258  bj-nnelirr  16316  subctctexmid  16366  nninfsellemeq  16380  ismkvnnlem  16420