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:  annotanannot  676  stbid  840  dcbid  846  con1biidc  885  pm4.54dc  910  ifpbi123d  1001  xorbi2d  1425  xorbi1d  1426  pm5.18im  1430  pm5.24dc  1443  neeq1  2427  neeq2  2428  necon3abid  2453  neleq1  2513  neleq2  2514  cdeqnot  3032  ru  3043  sbcng  3085  sbcnel12g  3157  sbcne12g  3158  difjust  3214  eldif  3222  dfdif3  3331  difeq2  3333  disjne  3564  eldifpr  3718  eldiftp  3737  prel12  3877  nalset  4242  pwnss  4274  poeq1  4422  pocl  4426  swopo  4429  sotritrieq  4448  tz7.2  4477  regexmidlem1  4657  regexmid  4659  nordeq  4668  nlimsucg  4690  nndceq0  4742  nnregexmid  4745  poinxp  4821  posng  4824  intirr  5151  poirr2  5157  cnvpom  5307  fndmdif  5785  isopolem  5997  canth  6003  poxp  6430  nnmword  6753  brdifun  6796  swoer  6797  2dom  7048  pw2f1odclem  7089  php5  7114  php5dom  7119  findcard2s  7149  fimax2gtrilemstep  7160  fimax2gtri  7161  fidcenumlemrk  7226  supeq3  7283  supeq123d  7284  supmoti  7286  eqsupti  7289  supubti  7292  supsnti  7298  isotilem  7299  isoti  7300  supisolem  7301  supisoex  7302  cnvinfex  7311  cnvti  7312  eqinfti  7313  infvalti  7315  difinfsn  7393  ismkv  7446  ismkvnex  7448  mkvprop  7451  fodjumkvlemres  7452  enmkvlem  7454  onntri35  7549  onntri45  7553  papirr  7562  tapeq1  7568  netap  7570  2omotaplemap  7573  exmidapne  7576  pitric  7638  addnidpig  7653  ltsonq  7715  elinp  7791  prltlu  7804  prdisj  7809  ltexprlemdisj  7923  suplocexpr  8042  ltposr  8080  aptisr  8096  suplocsrlem  8125  axpre-ltirr  8199  axpre-apti  8202  axpre-suploclemres  8218  axpre-suploc  8219  xrlenlt  8340  axapti  8346  axsuploc  8348  lttri3  8355  ltne  8360  leadd1  8706  reapti  8855  lemul1  8869  apirr  8881  apti  8898  apcon4bid  8900  lediv1  9145  lemuldiv  9157  lerec  9160  le2msq  9177  suprnubex  9229  suprleubex  9230  avgle1  9481  avgle2  9482  znnnlt1  9627  supinfneg  9930  infsupneg  9931  infregelbex  9933  eluzdc  9945  qapne  9974  xrltne  10149  xleneg  10173  nn0disj  10476  nelfzo  10490  elfzonelfzo  10579  fvinim0ffz  10591  zsupcllemstep  10593  zsupcllemex  10594  zsupssdc  10602  ioo0  10623  ico0  10625  ioc0  10626  flqlt  10647  expeq0  10936  nn0leexp2  11076  hashfibc  11211  leisorel  11213  wrdsymb0  11261  swrdnd  11355  maxleim  11894  maxabslemval  11897  maxleast  11902  minmax  11919  xrmaxleim  11933  xrmaxiflemval  11939  xrmaxlesup  11948  xrminmax  11954  summodclem3  12070  zeo3  12558  odd2np1  12563  mod2eq1n2dvds  12569  ndvdsadd  12621  fldivndvdslt  12627  bitsfval  12632  bitsval  12633  bits0  12638  bitsp1  12641  bitsmod  12646  bitscmp  12648  bitsinv1lem  12651  gcdneg  12682  nninfctlemfo  12740  algcvgblem  12750  lcmneg  12775  isprm3  12819  dvdsnprmd  12826  isprm5lem  12842  isprm5  12843  rpexp  12854  pw2dvdslemn  12866  pw2dvdseu  12869  oddpwdclemxy  12870  oddpwdclemdc  12874  oddpwdc  12875  sqpweven  12876  2sqpwodd  12877  sqne2sq  12878  phiprmpw  12923  m1dvdsndvds  12950  pythagtrip  12985  pcgcd1  13030  prmpwdvds  13057  ballotfilem2  13149  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemodife  13158  ballotfilem4  13159  oddennn  13160  ctinfomlemom  13195  ctinfom  13196  isnsgrp  13636  nzrunit  14350  bdxmet  15383  dedekindeulemlu  15503  suplociccex  15507  dedekindicclemlu  15512  efle  15658  logleb  15757  cxple  15799  cxple3  15803  lgsmod  15916  lgsdir2lem2  15919  lgsdir2  15923  lgsne0  15928  lgsprme0  15932  lgsquadlem1  15967  2lgslem3  15991  2lgsoddprm  16003  vtxd0nedgbfi  16311  1hevtxdg0fi  16319  eupth2lem3lem3fi  16482  eupth2lem3lem6fi  16483  eupth2lem3lem4fi  16485  eupth2lem3lem7fi  16486  eupth2lemsfi  16490  eupth2fi  16491  konigsberglem4  16503  decidi  16584  uzdcinzz  16587  bj-charfunbi  16598  bj-nalset  16682  bj-nnelirr  16740  subctctexmid  16791  exmidnotnotr  16796  exmidcon  16797  nninfsellemeq  16809  ismkvnnlem  16854