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  3273  difeq2  3275  disjne  3504  eldifpr  3649  eldiftp  3668  prel12  3801  nalset  4163  pwnss  4192  poeq1  4334  pocl  4338  swopo  4341  sotritrieq  4360  tz7.2  4389  regexmidlem1  4569  regexmid  4571  nordeq  4580  nlimsucg  4602  nndceq0  4654  nnregexmid  4657  poinxp  4732  posng  4735  intirr  5056  poirr2  5062  cnvpom  5212  fndmdif  5667  isopolem  5869  canth  5875  poxp  6290  nnmword  6576  brdifun  6619  swoer  6620  2dom  6864  pw2f1odclem  6895  php5  6919  php5dom  6924  findcard2s  6951  fimax2gtrilemstep  6961  fimax2gtri  6962  fidcenumlemrk  7020  supeq3  7056  supeq123d  7057  supmoti  7059  eqsupti  7062  supubti  7065  supsnti  7071  isotilem  7072  isoti  7073  supisolem  7074  supisoex  7075  cnvinfex  7084  cnvti  7085  eqinfti  7086  infvalti  7088  difinfsn  7166  ismkv  7219  ismkvnex  7221  mkvprop  7224  fodjumkvlemres  7225  enmkvlem  7227  onntri35  7304  onntri45  7308  tapeq1  7319  netap  7321  2omotaplemap  7324  exmidapne  7327  pitric  7388  addnidpig  7403  ltsonq  7465  elinp  7541  prltlu  7554  prdisj  7559  ltexprlemdisj  7673  suplocexpr  7792  ltposr  7830  aptisr  7846  suplocsrlem  7875  axpre-ltirr  7949  axpre-apti  7952  axpre-suploclemres  7968  axpre-suploc  7969  xrlenlt  8091  axapti  8097  axsuploc  8099  lttri3  8106  ltne  8111  leadd1  8457  reapti  8606  lemul1  8620  apirr  8632  apti  8649  apcon4bid  8651  lediv1  8896  lemuldiv  8908  lerec  8911  le2msq  8928  suprnubex  8980  suprleubex  8981  avgle1  9232  avgle2  9233  znnnlt1  9374  supinfneg  9669  infsupneg  9670  infregelbex  9672  eluzdc  9684  qapne  9713  xrltne  9888  xleneg  9912  nn0disj  10213  nelfzo  10227  elfzonelfzo  10306  fvinim0ffz  10317  zsupcllemstep  10319  zsupcllemex  10320  zsupssdc  10328  ioo0  10349  ico0  10351  ioc0  10352  flqlt  10373  expeq0  10662  nn0leexp2  10802  leisorel  10929  wrdsymb0  10967  maxleim  11370  maxabslemval  11373  maxleast  11378  minmax  11395  xrmaxleim  11409  xrmaxiflemval  11415  xrmaxlesup  11424  xrminmax  11430  summodclem3  11545  zeo3  12033  odd2np1  12038  mod2eq1n2dvds  12044  ndvdsadd  12096  fldivndvdslt  12102  bitsfval  12107  bitsval  12108  bits0  12112  bitsp1  12115  gcdneg  12149  nninfctlemfo  12207  algcvgblem  12217  lcmneg  12242  isprm3  12286  dvdsnprmd  12293  isprm5lem  12309  isprm5  12310  rpexp  12321  pw2dvdslemn  12333  pw2dvdseu  12336  oddpwdclemxy  12337  oddpwdclemdc  12341  oddpwdc  12342  sqpweven  12343  2sqpwodd  12344  sqne2sq  12345  phiprmpw  12390  m1dvdsndvds  12417  pythagtrip  12452  pcgcd1  12497  prmpwdvds  12524  oddennn  12609  ctinfomlemom  12644  ctinfom  12645  isnsgrp  13049  nzrunit  13744  bdxmet  14737  dedekindeulemlu  14857  suplociccex  14861  dedekindicclemlu  14866  efle  15012  logleb  15111  cxple  15153  cxple3  15157  lgsmod  15267  lgsdir2lem2  15270  lgsdir2  15274  lgsne0  15279  lgsprme0  15283  lgsquadlem1  15318  2lgslem3  15342  2lgsoddprm  15354  decidi  15441  uzdcinzz  15444  bj-charfunbi  15457  bj-nalset  15541  bj-nnelirr  15599  subctctexmid  15645  nninfsellemeq  15658  ismkvnnlem  15696