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:  annotanannot  676  stbid  840  dcbid  846  con1biidc  885  pm4.54dc  910  ifpbi123d  1001  xorbi2d  1425  xorbi1d  1426  pm5.18im  1430  pm5.24dc  1443  neeq1  2427  neeq2  2428  necon3abid  2453  neleq1  2513  neleq2  2514  cdeqnot  3033  ru  3044  sbcng  3086  sbcnel12g  3158  sbcne12g  3159  difjust  3215  eldif  3223  dfdif3  3333  difeq2  3335  disjne  3566  ifeqeqxdc  3673  eldifpr  3721  eldiftp  3740  prel12  3880  nalset  4245  pwnss  4277  poeq1  4425  pocl  4429  swopo  4432  sotritrieq  4451  tz7.2  4480  regexmidlem1  4660  regexmid  4662  nordeq  4671  nlimsucg  4693  nndceq0  4745  nnregexmid  4748  poinxp  4824  posng  4827  intirr  5154  poirr2  5160  cnvpom  5310  fndmdif  5788  isopolem  6001  canth  6009  poxp  6441  nnmword  6764  brdifun  6807  swoer  6808  2dom  7059  pw2f1odclem  7100  php5  7125  php5dom  7130  findcard2s  7160  fimax2gtrilemstep  7171  fimax2gtri  7172  fidcenumlemrk  7237  supeq3  7294  supeq123d  7295  supmoti  7297  eqsupti  7300  supubti  7303  supsnti  7309  isotilem  7310  isoti  7311  supisolem  7312  supisoex  7313  cnvinfex  7322  cnvti  7323  eqinfti  7324  infvalti  7326  difinfsn  7404  ismkv  7457  ismkvnex  7459  mkvprop  7462  fodjumkvlemres  7463  enmkvlem  7465  onntri35  7560  onntri45  7564  papeq1  7573  papirr  7575  tapeq1  7582  netap  7584  2omotaplemap  7587  exmidapne  7590  pitric  7652  addnidpig  7667  ltsonq  7729  elinp  7805  prltlu  7818  prdisj  7823  ltexprlemdisj  7937  suplocexpr  8056  ltposr  8094  aptisr  8110  suplocsrlem  8139  axpre-ltirr  8213  axpre-apti  8216  axpre-suploclemres  8232  axpre-suploc  8233  xrlenlt  8354  axapti  8360  axsuploc  8362  lttri3  8369  ltne  8374  leadd1  8721  reapti  8870  lemul1  8884  apirr  8896  apti  8913  apcon4bid  8915  lediv1  9160  lemuldiv  9172  lerec  9175  le2msq  9192  suprnubex  9244  suprleubex  9245  avgle1  9496  avgle2  9497  znnnlt1  9642  supinfneg  9945  infsupneg  9946  infregelbex  9948  eluzdc  9960  qapne  9989  xrltne  10165  xleneg  10189  nn0disj  10494  nelfzo  10508  elfzonelfzo  10597  fvinim0ffz  10609  zsupcllemstep  10611  zsupcllemex  10612  zsupssdc  10622  ioo0  10643  ico0  10645  ioc0  10646  flqlt  10667  expeq0  10956  nn0leexp2  11097  hashfibc  11232  leisorel  11234  wrdsymb0  11282  swrdnd  11376  maxleim  11915  maxabslemval  11918  maxleast  11923  minmax  11940  xrmaxleim  11954  xrmaxiflemval  11960  xrmaxlesup  11969  xrminmax  11975  summodclem3  12091  zeo3  12579  odd2np1  12584  mod2eq1n2dvds  12590  ndvdsadd  12642  fldivndvdslt  12648  bitsfval  12653  bitsval  12654  bits0  12659  bitsp1  12662  bitsmod  12667  bitscmp  12669  bitsinv1lem  12672  gcdneg  12703  nninfctlemfo  12761  algcvgblem  12771  lcmneg  12796  isprm3  12840  dvdsnprmd  12847  isprm5lem  12863  isprm5  12864  rpexp  12875  pw2dvdslemn  12887  pw2dvdseu  12890  oddpwdclemxy  12891  oddpwdclemdc  12895  oddpwdc  12896  sqpweven  12897  2sqpwodd  12898  sqne2sq  12899  phiprmpw  12944  m1dvdsndvds  12971  pythagtrip  13006  pcgcd1  13051  prmpwdvds  13078  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilem4  13185  ballotfilem7  13223  oddennn  13227  ctinfomlemom  13262  ctinfom  13263  isnsgrp  13669  nzrunit  14433  opprdrng  14558  bdxmet  15492  dedekindeulemlu  15612  suplociccex  15616  dedekindicclemlu  15621  efle  15767  logleb  15866  cxple  15908  cxple3  15912  lgsmod  16025  lgsdir2lem2  16028  lgsdir2  16032  lgsne0  16037  lgsprme0  16041  lgsquadlem1  16076  2lgslem3  16100  2lgsoddprm  16112  vtxd0nedgbfi  16420  1hevtxdg0fi  16428  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  eupth2lemsfi  16599  eupth2fi  16600  konigsberglem4  16612  decidi  16693  uzdcinzz  16696  bj-charfunbi  16707  bj-nalset  16791  bj-nnelirr  16849  subctctexmid  16900  exmidnotnotr  16905  exmidcon  16906  nninfsellemeq  16918  ismkvnnlem  16963