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  5668  isopolem  5870  canth  5876  poxp  6291  nnmword  6577  brdifun  6620  swoer  6621  2dom  6865  pw2f1odclem  6896  php5  6920  php5dom  6925  findcard2s  6952  fimax2gtrilemstep  6962  fimax2gtri  6963  fidcenumlemrk  7021  supeq3  7057  supeq123d  7058  supmoti  7060  eqsupti  7063  supubti  7066  supsnti  7072  isotilem  7073  isoti  7074  supisolem  7075  supisoex  7076  cnvinfex  7085  cnvti  7086  eqinfti  7087  infvalti  7089  difinfsn  7167  ismkv  7220  ismkvnex  7222  mkvprop  7225  fodjumkvlemres  7226  enmkvlem  7228  onntri35  7306  onntri45  7310  tapeq1  7321  netap  7323  2omotaplemap  7326  exmidapne  7329  pitric  7390  addnidpig  7405  ltsonq  7467  elinp  7543  prltlu  7556  prdisj  7561  ltexprlemdisj  7675  suplocexpr  7794  ltposr  7832  aptisr  7848  suplocsrlem  7877  axpre-ltirr  7951  axpre-apti  7954  axpre-suploclemres  7970  axpre-suploc  7971  xrlenlt  8093  axapti  8099  axsuploc  8101  lttri3  8108  ltne  8113  leadd1  8459  reapti  8608  lemul1  8622  apirr  8634  apti  8651  apcon4bid  8653  lediv1  8898  lemuldiv  8910  lerec  8913  le2msq  8930  suprnubex  8982  suprleubex  8983  avgle1  9234  avgle2  9235  znnnlt1  9376  supinfneg  9671  infsupneg  9672  infregelbex  9674  eluzdc  9686  qapne  9715  xrltne  9890  xleneg  9914  nn0disj  10215  nelfzo  10229  elfzonelfzo  10308  fvinim0ffz  10319  zsupcllemstep  10321  zsupcllemex  10322  zsupssdc  10330  ioo0  10351  ico0  10353  ioc0  10354  flqlt  10375  expeq0  10664  nn0leexp2  10804  leisorel  10931  wrdsymb0  10969  maxleim  11372  maxabslemval  11375  maxleast  11380  minmax  11397  xrmaxleim  11411  xrmaxiflemval  11417  xrmaxlesup  11426  xrminmax  11432  summodclem3  11547  zeo3  12035  odd2np1  12040  mod2eq1n2dvds  12046  ndvdsadd  12098  fldivndvdslt  12104  bitsfval  12109  bitsval  12110  bits0  12115  bitsp1  12118  bitsmod  12123  bitscmp  12125  bitsinv1lem  12128  gcdneg  12159  nninfctlemfo  12217  algcvgblem  12227  lcmneg  12252  isprm3  12296  dvdsnprmd  12303  isprm5lem  12319  isprm5  12320  rpexp  12331  pw2dvdslemn  12343  pw2dvdseu  12346  oddpwdclemxy  12347  oddpwdclemdc  12351  oddpwdc  12352  sqpweven  12353  2sqpwodd  12354  sqne2sq  12355  phiprmpw  12400  m1dvdsndvds  12427  pythagtrip  12462  pcgcd1  12507  prmpwdvds  12534  oddennn  12619  ctinfomlemom  12654  ctinfom  12655  isnsgrp  13059  nzrunit  13754  bdxmet  14747  dedekindeulemlu  14867  suplociccex  14871  dedekindicclemlu  14876  efle  15022  logleb  15121  cxple  15163  cxple3  15167  lgsmod  15277  lgsdir2lem2  15280  lgsdir2  15284  lgsne0  15289  lgsprme0  15293  lgsquadlem1  15328  2lgslem3  15352  2lgsoddprm  15364  decidi  15451  uzdcinzz  15454  bj-charfunbi  15467  bj-nalset  15551  bj-nnelirr  15609  subctctexmid  15655  nninfsellemeq  15668  ismkvnnlem  15706