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  2377  neeq2  2378  necon3abid  2403  neleq1  2463  neleq2  2464  cdeqnot  2974  ru  2985  sbcng  3027  sbcnel12g  3098  sbcne12g  3099  difjust  3155  eldif  3163  dfdif3  3270  difeq2  3272  disjne  3501  eldifpr  3646  eldiftp  3665  prel12  3798  nalset  4160  pwnss  4189  poeq1  4331  pocl  4335  swopo  4338  sotritrieq  4357  tz7.2  4386  regexmidlem1  4566  regexmid  4568  nordeq  4577  nlimsucg  4599  nndceq0  4651  nnregexmid  4654  poinxp  4729  posng  4732  intirr  5053  poirr2  5059  cnvpom  5209  fndmdif  5664  isopolem  5866  canth  5872  poxp  6287  nnmword  6573  brdifun  6616  swoer  6617  2dom  6861  pw2f1odclem  6892  php5  6916  php5dom  6921  findcard2s  6948  fimax2gtrilemstep  6958  fimax2gtri  6959  fidcenumlemrk  7015  supeq3  7051  supeq123d  7052  supmoti  7054  eqsupti  7057  supubti  7060  supsnti  7066  isotilem  7067  isoti  7068  supisolem  7069  supisoex  7070  cnvinfex  7079  cnvti  7080  eqinfti  7081  infvalti  7083  difinfsn  7161  ismkv  7214  ismkvnex  7216  mkvprop  7219  fodjumkvlemres  7220  enmkvlem  7222  onntri35  7299  onntri45  7303  tapeq1  7314  netap  7316  2omotaplemap  7319  exmidapne  7322  pitric  7383  addnidpig  7398  ltsonq  7460  elinp  7536  prltlu  7549  prdisj  7554  ltexprlemdisj  7668  suplocexpr  7787  ltposr  7825  aptisr  7841  suplocsrlem  7870  axpre-ltirr  7944  axpre-apti  7947  axpre-suploclemres  7963  axpre-suploc  7964  xrlenlt  8086  axapti  8092  axsuploc  8094  lttri3  8101  ltne  8106  leadd1  8451  reapti  8600  lemul1  8614  apirr  8626  apti  8643  apcon4bid  8645  lediv1  8890  lemuldiv  8902  lerec  8905  le2msq  8922  suprnubex  8974  suprleubex  8975  avgle1  9226  avgle2  9227  znnnlt1  9368  supinfneg  9663  infsupneg  9664  infregelbex  9666  eluzdc  9678  qapne  9707  xrltne  9882  xleneg  9906  nn0disj  10207  nelfzo  10221  elfzonelfzo  10300  fvinim0ffz  10311  ioo0  10331  ico0  10333  ioc0  10334  flqlt  10355  expeq0  10644  nn0leexp2  10784  leisorel  10911  wrdsymb0  10949  maxleim  11352  maxabslemval  11355  maxleast  11360  minmax  11376  xrmaxleim  11390  xrmaxiflemval  11396  xrmaxlesup  11405  xrminmax  11411  summodclem3  11526  zeo3  12012  odd2np1  12017  mod2eq1n2dvds  12023  ndvdsadd  12075  fldivndvdslt  12079  zsupcllemstep  12085  zsupcllemex  12086  zsupssdc  12094  gcdneg  12122  nninfctlemfo  12180  algcvgblem  12190  lcmneg  12215  isprm3  12259  dvdsnprmd  12266  isprm5lem  12282  isprm5  12283  rpexp  12294  pw2dvdslemn  12306  pw2dvdseu  12309  oddpwdclemxy  12310  oddpwdclemdc  12314  oddpwdc  12315  sqpweven  12316  2sqpwodd  12317  sqne2sq  12318  phiprmpw  12363  m1dvdsndvds  12389  pythagtrip  12424  pcgcd1  12469  prmpwdvds  12496  oddennn  12552  ctinfomlemom  12587  ctinfom  12588  isnsgrp  12992  nzrunit  13687  bdxmet  14680  dedekindeulemlu  14800  suplociccex  14804  dedekindicclemlu  14809  efle  14952  logleb  15051  cxple  15092  cxple3  15096  lgsmod  15183  lgsdir2lem2  15186  lgsdir2  15190  lgsne0  15195  lgsprme0  15199  lgsquadlem1  15234  2lgslem3  15258  2lgsoddprm  15270  decidi  15357  uzdcinzz  15360  bj-charfunbi  15373  bj-nalset  15457  bj-nnelirr  15515  subctctexmid  15561  nninfsellemeq  15574  ismkvnnlem  15612