Theorem notbid 662

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  827  dcbid  833  con1biidc  872  pm4.54dc  897  xorbi2d  1375  xorbi1d  1376  pm5.18im  1380  pm5.24dc  1393  neeq1  2353  neeq2  2354  necon3abid  2379  neleq1  2439  neleq2  2440  cdeqnot  2943  ru  2954  sbcng  2995  sbcnel12g  3066  sbcne12g  3067  difjust  3122  eldif  3130  dfdif3  3237  difeq2  3239  disjne  3468  eldifpr  3610  eldiftp  3629  prel12  3758  nalset  4119  pwnss  4145  poeq1  4284  pocl  4288  swopo  4291  sotritrieq  4310  tz7.2  4339  regexmidlem1  4517  regexmid  4519  nordeq  4528  nlimsucg  4550  nndceq0  4602  nnregexmid  4605  poinxp  4680  posng  4683  intirr  4997  poirr2  5003  cnvpom  5153  fndmdif  5601  isopolem  5801  canth  5807  poxp  6211  nnmword  6497  brdifun  6540  swoer  6541  2dom  6783  php5  6836  php5dom  6841  findcard2s  6868  fimax2gtrilemstep  6878  fimax2gtri  6879  fidcenumlemrk  6931  supeq3  6967  supeq123d  6968  supmoti  6970  eqsupti  6973  supubti  6976  supsnti  6982  isotilem  6983  isoti  6984  supisolem  6985  supisoex  6986  cnvinfex  6995  cnvti  6996  eqinfti  6997  infvalti  6999  difinfsn  7077  ismkv  7129  ismkvnex  7131  mkvprop  7134  fodjumkvlemres  7135  enmkvlem  7137  onntri35  7214  onntri45  7218  pitric  7283  addnidpig  7298  ltsonq  7360  elinp  7436  prltlu  7449  prdisj  7454  ltexprlemdisj  7568  suplocexpr  7687  ltposr  7725  aptisr  7741  suplocsrlem  7770  axpre-ltirr  7844  axpre-apti  7847  axpre-suploclemres  7863  axpre-suploc  7864  xrlenlt  7984  axapti  7990  axsuploc  7992  lttri3  7999  ltne  8004  leadd1  8349  reapti  8498  lemul1  8512  apirr  8524  apti  8541  apcon4bid  8543  lediv1  8785  lemuldiv  8797  lerec  8800  le2msq  8817  suprnubex  8869  suprleubex  8870  avgle1  9118  avgle2  9119  znnnlt1  9260  supinfneg  9554  infsupneg  9555  infregelbex  9557  eluzdc  9569  qapne  9598  xrltne  9770  xleneg  9794  nn0disj  10094  elfzonelfzo  10186  fvinim0ffz  10197  ioo0  10216  ico0  10218  ioc0  10219  flqlt  10239  expeq0  10507  nn0leexp2  10645  leisorel  10772  maxleim  11169  maxabslemval  11172  maxleast  11177  minmax  11193  xrmaxleim  11207  xrmaxiflemval  11213  xrmaxlesup  11222  xrminmax  11228  summodclem3  11343  zeo3  11827  odd2np1  11832  mod2eq1n2dvds  11838  ndvdsadd  11890  fldivndvdslt  11894  zsupcllemstep  11900  zsupcllemex  11901  zsupssdc  11909  gcdneg  11937  algcvgblem  12003  lcmneg  12028  isprm3  12072  dvdsnprmd  12079  isprm5lem  12095  isprm5  12096  rpexp  12107  pw2dvdslemn  12119  pw2dvdseu  12122  oddpwdclemxy  12123  oddpwdclemdc  12127  oddpwdc  12128  sqpweven  12129  2sqpwodd  12130  sqne2sq  12131  phiprmpw  12176  m1dvdsndvds  12202  pythagtrip  12237  pcgcd1  12281  prmpwdvds  12307  oddennn  12347  ctinfomlemom  12382  ctinfom  12383  isnsgrp  12647  bdxmet  13295  dedekindeulemlu  13393  suplociccex  13397  dedekindicclemlu  13402  efle  13491  logleb  13590  cxple  13631  cxple3  13635  lgsmod  13721  lgsdir2lem2  13724  lgsdir2  13728  lgsne0  13733  lgsprme0  13737  decidi  13830  uzdcinzz  13833  bj-charfunbi  13846  bj-nalset  13930  bj-nnelirr  13988  subctctexmid  14034  nninfsellemeq  14047  ismkvnnlem  14084