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  2373  neeq2  2374  necon3abid  2399  neleq1  2459  neleq2  2460  cdeqnot  2965  ru  2976  sbcng  3018  sbcnel12g  3089  sbcne12g  3090  difjust  3145  eldif  3153  dfdif3  3260  difeq2  3262  disjne  3491  eldifpr  3634  eldiftp  3653  prel12  3786  nalset  4148  pwnss  4174  poeq1  4314  pocl  4318  swopo  4321  sotritrieq  4340  tz7.2  4369  regexmidlem1  4547  regexmid  4549  nordeq  4558  nlimsucg  4580  nndceq0  4632  nnregexmid  4635  poinxp  4710  posng  4713  intirr  5030  poirr2  5036  cnvpom  5186  fndmdif  5637  isopolem  5839  canth  5845  poxp  6251  nnmword  6537  brdifun  6580  swoer  6581  2dom  6823  php5  6876  php5dom  6881  findcard2s  6908  fimax2gtrilemstep  6918  fimax2gtri  6919  fidcenumlemrk  6971  supeq3  7007  supeq123d  7008  supmoti  7010  eqsupti  7013  supubti  7016  supsnti  7022  isotilem  7023  isoti  7024  supisolem  7025  supisoex  7026  cnvinfex  7035  cnvti  7036  eqinfti  7037  infvalti  7039  difinfsn  7117  ismkv  7169  ismkvnex  7171  mkvprop  7174  fodjumkvlemres  7175  enmkvlem  7177  onntri35  7254  onntri45  7258  tapeq1  7269  netap  7271  2omotaplemap  7274  exmidapne  7277  pitric  7338  addnidpig  7353  ltsonq  7415  elinp  7491  prltlu  7504  prdisj  7509  ltexprlemdisj  7623  suplocexpr  7742  ltposr  7780  aptisr  7796  suplocsrlem  7825  axpre-ltirr  7899  axpre-apti  7902  axpre-suploclemres  7918  axpre-suploc  7919  xrlenlt  8040  axapti  8046  axsuploc  8048  lttri3  8055  ltne  8060  leadd1  8405  reapti  8554  lemul1  8568  apirr  8580  apti  8597  apcon4bid  8599  lediv1  8844  lemuldiv  8856  lerec  8859  le2msq  8876  suprnubex  8928  suprleubex  8929  avgle1  9177  avgle2  9178  znnnlt1  9319  supinfneg  9613  infsupneg  9614  infregelbex  9616  eluzdc  9628  qapne  9657  xrltne  9831  xleneg  9855  nn0disj  10156  elfzonelfzo  10248  fvinim0ffz  10259  ioo0  10278  ico0  10280  ioc0  10281  flqlt  10301  expeq0  10569  nn0leexp2  10708  leisorel  10835  maxleim  11232  maxabslemval  11235  maxleast  11240  minmax  11256  xrmaxleim  11270  xrmaxiflemval  11276  xrmaxlesup  11285  xrminmax  11291  summodclem3  11406  zeo3  11891  odd2np1  11896  mod2eq1n2dvds  11902  ndvdsadd  11954  fldivndvdslt  11958  zsupcllemstep  11964  zsupcllemex  11965  zsupssdc  11973  gcdneg  12001  algcvgblem  12067  lcmneg  12092  isprm3  12136  dvdsnprmd  12143  isprm5lem  12159  isprm5  12160  rpexp  12171  pw2dvdslemn  12183  pw2dvdseu  12186  oddpwdclemxy  12187  oddpwdclemdc  12191  oddpwdc  12192  sqpweven  12193  2sqpwodd  12194  sqne2sq  12195  phiprmpw  12240  m1dvdsndvds  12266  pythagtrip  12301  pcgcd1  12345  prmpwdvds  12371  oddennn  12411  ctinfomlemom  12446  ctinfom  12447  isnsgrp  12835  nzrunit  13496  bdxmet  14398  dedekindeulemlu  14496  suplociccex  14500  dedekindicclemlu  14505  efle  14594  logleb  14693  cxple  14734  cxple3  14738  lgsmod  14824  lgsdir2lem2  14827  lgsdir2  14831  lgsne0  14836  lgsprme0  14840  decidi  14944  uzdcinzz  14947  bj-charfunbi  14960  bj-nalset  15044  bj-nnelirr  15102  subctctexmid  15148  nninfsellemeq  15161  ismkvnnlem  15198