Theorem notbid 657

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 656	. 2 |- ( ( ps <-> ch ) -> ( -. ps <-> -. ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( -. ps <-> -. ch ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  818  dcbid  824  con1biidc  863  pm4.54dc  888  xorbi2d  1359  xorbi1d  1360  pm5.18im  1364  pm5.24dc  1377  neeq1  2322  neeq2  2323  necon3abid  2348  neleq1  2408  neleq2  2409  cdeqnot  2901  ru  2912  sbcng  2953  sbcnel12g  3024  sbcne12g  3025  difjust  3077  eldif  3085  dfdif3  3191  difeq2  3193  disjne  3421  eldifpr  3559  eldiftp  3577  prel12  3706  nalset  4066  pwnss  4091  poeq1  4229  pocl  4233  swopo  4236  sotritrieq  4255  tz7.2  4284  regexmidlem1  4456  regexmid  4458  nordeq  4467  nlimsucg  4489  nndceq0  4539  nnregexmid  4542  poinxp  4616  posng  4619  intirr  4933  poirr2  4939  cnvpom  5089  fndmdif  5533  isopolem  5731  poxp  6137  nnmword  6422  brdifun  6464  swoer  6465  2dom  6707  php5  6760  php5dom  6765  findcard2s  6792  fimax2gtrilemstep  6802  fimax2gtri  6803  fidcenumlemrk  6850  supeq3  6885  supeq123d  6886  supmoti  6888  eqsupti  6891  supubti  6894  supsnti  6900  isotilem  6901  isoti  6902  supisolem  6903  supisoex  6904  cnvinfex  6913  cnvti  6914  eqinfti  6915  infvalti  6917  difinfsn  6993  ismkv  7035  ismkvnex  7037  mkvprop  7040  fodjumkvlemres  7041  enmkvlem  7043  pitric  7153  addnidpig  7168  ltsonq  7230  elinp  7306  prltlu  7319  prdisj  7324  ltexprlemdisj  7438  suplocexpr  7557  ltposr  7595  aptisr  7611  suplocsrlem  7640  axpre-ltirr  7714  axpre-apti  7717  axpre-suploclemres  7733  axpre-suploc  7734  xrlenlt  7853  axapti  7859  axsuploc  7861  lttri3  7868  ltne  7873  leadd1  8216  reapti  8365  lemul1  8379  apirr  8391  apti  8408  apcon4bid  8410  lediv1  8651  lemuldiv  8663  lerec  8666  le2msq  8683  suprnubex  8735  suprleubex  8736  avgle1  8984  avgle2  8985  znnnlt1  9126  supinfneg  9417  infsupneg  9418  eluzdc  9431  qapne  9458  xrltne  9626  xleneg  9650  nn0disj  9946  elfzonelfzo  10038  fvinim0ffz  10049  ioo0  10068  ico0  10070  ioc0  10071  flqlt  10087  expeq0  10355  leisorel  10612  maxleim  11009  maxabslemval  11012  maxleast  11017  minmax  11033  xrmaxleim  11045  xrmaxiflemval  11051  xrmaxlesup  11060  xrminmax  11066  summodclem3  11181  zeo3  11601  odd2np1  11606  mod2eq1n2dvds  11612  ndvdsadd  11664  fldivndvdslt  11668  zsupcllemstep  11674  zsupcllemex  11675  gcdneg  11706  algcvgblem  11766  lcmneg  11791  isprm3  11835  dvdsnprmd  11842  rpexp  11867  pw2dvdslemn  11879  pw2dvdseu  11882  oddpwdclemxy  11883  oddpwdclemdc  11887  oddpwdc  11888  sqpweven  11889  2sqpwodd  11890  sqne2sq  11891  phiprmpw  11934  oddennn  11941  ctinfomlemom  11976  ctinfom  11977  bdxmet  12709  dedekindeulemlu  12807  suplociccex  12811  dedekindicclemlu  12816  efle  12905  logleb  13004  cxple  13045  cxple3  13049  decidi  13173  uzdcinzz  13176  bj-nalset  13264  bj-nnelirr  13322  subctctexmid  13369  nninfsellemeq  13385  ismkvnnlem  13419