Theorem notbid 673

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 672	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  839  dcbid  845  con1biidc  884  pm4.54dc  909  ifpbi123d  1000  xorbi2d  1424  xorbi1d  1425  pm5.18im  1429  pm5.24dc  1442  neeq1  2415  neeq2  2416  necon3abid  2441  neleq1  2501  neleq2  2502  cdeqnot  3019  ru  3030  sbcng  3072  sbcnel12g  3144  sbcne12g  3145  difjust  3201  eldif  3209  dfdif3  3317  difeq2  3319  disjne  3548  eldifpr  3696  eldiftp  3715  prel12  3854  nalset  4219  pwnss  4249  poeq1  4396  pocl  4400  swopo  4403  sotritrieq  4422  tz7.2  4451  regexmidlem1  4631  regexmid  4633  nordeq  4642  nlimsucg  4664  nndceq0  4716  nnregexmid  4719  poinxp  4795  posng  4798  intirr  5123  poirr2  5129  cnvpom  5279  fndmdif  5752  isopolem  5962  canth  5968  poxp  6396  nnmword  6685  brdifun  6728  swoer  6729  2dom  6979  pw2f1odclem  7019  php5  7043  php5dom  7048  findcard2s  7078  fimax2gtrilemstep  7089  fimax2gtri  7090  fidcenumlemrk  7152  supeq3  7188  supeq123d  7189  supmoti  7191  eqsupti  7194  supubti  7197  supsnti  7203  isotilem  7204  isoti  7205  supisolem  7206  supisoex  7207  cnvinfex  7216  cnvti  7217  eqinfti  7218  infvalti  7220  difinfsn  7298  ismkv  7351  ismkvnex  7353  mkvprop  7356  fodjumkvlemres  7357  enmkvlem  7359  onntri35  7454  onntri45  7458  tapeq1  7470  netap  7472  2omotaplemap  7475  exmidapne  7478  pitric  7540  addnidpig  7555  ltsonq  7617  elinp  7693  prltlu  7706  prdisj  7711  ltexprlemdisj  7825  suplocexpr  7944  ltposr  7982  aptisr  7998  suplocsrlem  8027  axpre-ltirr  8101  axpre-apti  8104  axpre-suploclemres  8120  axpre-suploc  8121  xrlenlt  8243  axapti  8249  axsuploc  8251  lttri3  8258  ltne  8263  leadd1  8609  reapti  8758  lemul1  8772  apirr  8784  apti  8801  apcon4bid  8803  lediv1  9048  lemuldiv  9060  lerec  9063  le2msq  9080  suprnubex  9132  suprleubex  9133  avgle1  9384  avgle2  9385  znnnlt1  9526  supinfneg  9828  infsupneg  9829  infregelbex  9831  eluzdc  9843  qapne  9872  xrltne  10047  xleneg  10071  nn0disj  10372  nelfzo  10386  elfzonelfzo  10474  fvinim0ffz  10486  zsupcllemstep  10488  zsupcllemex  10489  zsupssdc  10497  ioo0  10518  ico0  10520  ioc0  10521  flqlt  10542  expeq0  10831  nn0leexp2  10971  leisorel  11100  wrdsymb0  11145  swrdnd  11239  maxleim  11765  maxabslemval  11768  maxleast  11773  minmax  11790  xrmaxleim  11804  xrmaxiflemval  11810  xrmaxlesup  11819  xrminmax  11825  summodclem3  11940  zeo3  12428  odd2np1  12433  mod2eq1n2dvds  12439  ndvdsadd  12491  fldivndvdslt  12497  bitsfval  12502  bitsval  12503  bits0  12508  bitsp1  12511  bitsmod  12516  bitscmp  12518  bitsinv1lem  12521  gcdneg  12552  nninfctlemfo  12610  algcvgblem  12620  lcmneg  12645  isprm3  12689  dvdsnprmd  12696  isprm5lem  12712  isprm5  12713  rpexp  12724  pw2dvdslemn  12736  pw2dvdseu  12739  oddpwdclemxy  12740  oddpwdclemdc  12744  oddpwdc  12745  sqpweven  12746  2sqpwodd  12747  sqne2sq  12748  phiprmpw  12793  m1dvdsndvds  12820  pythagtrip  12855  pcgcd1  12900  prmpwdvds  12927  oddennn  13012  ctinfomlemom  13047  ctinfom  13048  isnsgrp  13488  nzrunit  14201  bdxmet  15224  dedekindeulemlu  15344  suplociccex  15348  dedekindicclemlu  15353  efle  15499  logleb  15598  cxple  15640  cxple3  15644  lgsmod  15754  lgsdir2lem2  15757  lgsdir2  15761  lgsne0  15766  lgsprme0  15770  lgsquadlem1  15805  2lgslem3  15829  2lgsoddprm  15841  vtxd0nedgbfi  16149  1hevtxdg0fi  16157  decidi  16391  uzdcinzz  16394  bj-charfunbi  16406  bj-nalset  16490  bj-nnelirr  16548  subctctexmid  16601  nninfsellemeq  16616  ismkvnnlem  16656