Theorem notbid 669

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 668	. 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  834  dcbid  840  con1biidc  879  pm4.54dc  904  xorbi2d  1400  xorbi1d  1401  pm5.18im  1405  pm5.24dc  1418  neeq1  2391  neeq2  2392  necon3abid  2417  neleq1  2477  neleq2  2478  cdeqnot  2993  ru  3004  sbcng  3046  sbcnel12g  3118  sbcne12g  3119  difjust  3175  eldif  3183  dfdif3  3291  difeq2  3293  disjne  3522  eldifpr  3670  eldiftp  3689  prel12  3825  nalset  4190  pwnss  4219  poeq1  4364  pocl  4368  swopo  4371  sotritrieq  4390  tz7.2  4419  regexmidlem1  4599  regexmid  4601  nordeq  4610  nlimsucg  4632  nndceq0  4684  nnregexmid  4687  poinxp  4762  posng  4765  intirr  5088  poirr2  5094  cnvpom  5244  fndmdif  5708  isopolem  5914  canth  5920  poxp  6341  nnmword  6627  brdifun  6670  swoer  6671  2dom  6921  pw2f1odclem  6956  php5  6980  php5dom  6985  findcard2s  7013  fimax2gtrilemstep  7023  fimax2gtri  7024  fidcenumlemrk  7082  supeq3  7118  supeq123d  7119  supmoti  7121  eqsupti  7124  supubti  7127  supsnti  7133  isotilem  7134  isoti  7135  supisolem  7136  supisoex  7137  cnvinfex  7146  cnvti  7147  eqinfti  7148  infvalti  7150  difinfsn  7228  ismkv  7281  ismkvnex  7283  mkvprop  7286  fodjumkvlemres  7287  enmkvlem  7289  onntri35  7383  onntri45  7387  tapeq1  7399  netap  7401  2omotaplemap  7404  exmidapne  7407  pitric  7469  addnidpig  7484  ltsonq  7546  elinp  7622  prltlu  7635  prdisj  7640  ltexprlemdisj  7754  suplocexpr  7873  ltposr  7911  aptisr  7927  suplocsrlem  7956  axpre-ltirr  8030  axpre-apti  8033  axpre-suploclemres  8049  axpre-suploc  8050  xrlenlt  8172  axapti  8178  axsuploc  8180  lttri3  8187  ltne  8192  leadd1  8538  reapti  8687  lemul1  8701  apirr  8713  apti  8730  apcon4bid  8732  lediv1  8977  lemuldiv  8989  lerec  8992  le2msq  9009  suprnubex  9061  suprleubex  9062  avgle1  9313  avgle2  9314  znnnlt1  9455  supinfneg  9751  infsupneg  9752  infregelbex  9754  eluzdc  9766  qapne  9795  xrltne  9970  xleneg  9994  nn0disj  10295  nelfzo  10309  elfzonelfzo  10396  fvinim0ffz  10407  zsupcllemstep  10409  zsupcllemex  10410  zsupssdc  10418  ioo0  10439  ico0  10441  ioc0  10442  flqlt  10463  expeq0  10752  nn0leexp2  10892  leisorel  11019  wrdsymb0  11063  swrdnd  11150  maxleim  11631  maxabslemval  11634  maxleast  11639  minmax  11656  xrmaxleim  11670  xrmaxiflemval  11676  xrmaxlesup  11685  xrminmax  11691  summodclem3  11806  zeo3  12294  odd2np1  12299  mod2eq1n2dvds  12305  ndvdsadd  12357  fldivndvdslt  12363  bitsfval  12368  bitsval  12369  bits0  12374  bitsp1  12377  bitsmod  12382  bitscmp  12384  bitsinv1lem  12387  gcdneg  12418  nninfctlemfo  12476  algcvgblem  12486  lcmneg  12511  isprm3  12555  dvdsnprmd  12562  isprm5lem  12578  isprm5  12579  rpexp  12590  pw2dvdslemn  12602  pw2dvdseu  12605  oddpwdclemxy  12606  oddpwdclemdc  12610  oddpwdc  12611  sqpweven  12612  2sqpwodd  12613  sqne2sq  12614  phiprmpw  12659  m1dvdsndvds  12686  pythagtrip  12721  pcgcd1  12766  prmpwdvds  12793  oddennn  12878  ctinfomlemom  12913  ctinfom  12914  isnsgrp  13353  nzrunit  14065  bdxmet  15088  dedekindeulemlu  15208  suplociccex  15212  dedekindicclemlu  15217  efle  15363  logleb  15462  cxple  15504  cxple3  15508  lgsmod  15618  lgsdir2lem2  15621  lgsdir2  15625  lgsne0  15630  lgsprme0  15634  lgsquadlem1  15669  2lgslem3  15693  2lgsoddprm  15705  decidi  15931  uzdcinzz  15934  bj-charfunbi  15946  bj-nalset  16030  bj-nnelirr  16088  subctctexmid  16139  nninfsellemeq  16153  ismkvnnlem  16193