Theorem notbid 677

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 676	. 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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  annotanannot  680  stbid  844  dcbid  850  con1biidc  889  pm4.54dc  914  ifpbi123d  1005  xorbi2d  1429  xorbi1d  1430  pm5.18im  1434  pm5.24dc  1447  neeq1  2433  neeq2  2434  necon3abid  2459  neleq1  2519  neleq2  2520  cdeqnot  3039  ru  3050  sbcng  3092  sbcnel12g  3164  sbcne12g  3165  difjust  3221  eldif  3229  dfdif3  3339  difeq2  3341  disjne  3577  ifeqeqxdc  3684  eldifpr  3732  eldiftp  3751  prel12  3891  nalset  4258  pwnss  4291  poeq1  4439  pocl  4443  swopo  4446  sotritrieq  4465  tz7.2  4494  regexmidlem1  4675  regexmid  4677  nordeq  4686  nlimsucg  4708  nndceq0  4760  nnregexmid  4763  poinxp  4839  posng  4842  intirr  5169  poirr2  5175  cnvpom  5325  fndmdif  5805  isopolem  6018  canth  6026  poxp  6458  nnmword  6781  brdifun  6824  swoer  6825  2dom  7083  pw2f1odclem  7124  php5  7149  php5dom  7154  findcard2s  7184  fimax2gtrilemstep  7195  fimax2gtri  7196  fidcenumlemrk  7261  supeq3  7320  supeq123d  7321  supmoti  7323  eqsupti  7326  supubti  7329  supsnti  7335  isotilem  7336  isoti  7337  supisolem  7338  supisoex  7339  cnvinfex  7348  cnvti  7349  eqinfti  7350  infvalti  7352  difinfsn  7430  ismkv  7483  ismkvnex  7485  mkvprop  7488  fodjumkvlemres  7489  enmkvlem  7491  onntri35  7586  onntri45  7590  papeq1  7599  papirr  7601  tapeq1  7608  netap  7610  2omotaplemap  7613  exmidapne  7616  pitric  7678  addnidpig  7693  ltsonq  7755  elinp  7831  prltlu  7844  prdisj  7849  ltexprlemdisj  7963  suplocexpr  8082  ltposr  8120  aptisr  8136  suplocsrlem  8165  axpre-ltirr  8239  axpre-apti  8242  axpre-suploclemres  8258  axpre-suploc  8259  xrlenlt  8380  axapti  8386  axsuploc  8388  lttri3  8395  ltne  8400  leadd1  8748  reapti  8897  lemul1  8911  apirr  8923  apti  8940  apcon4bid  8942  lediv1  9189  lemuldiv  9201  lerec  9204  le2msq  9221  suprnubex  9273  suprleubex  9274  avgle1  9525  avgle2  9526  znnnlt1  9671  supinfneg  9974  infsupneg  9975  infregelbex  9977  eluzdc  9989  qapne  10018  xrltne  10194  xleneg  10218  nn0disj  10523  nelfzo  10537  elfzonelfzo  10626  fvinim0ffz  10638  zsupcllemstep  10640  zsupcllemex  10641  zsupssdc  10651  ioo0  10672  ico0  10674  ioc0  10675  flqlt  10696  expeq0  10985  nn0leexp2  11126  hashfibc  11261  leisorel  11267  wrdsymb0  11315  swrdnd  11409  maxleim  11949  maxabslemval  11952  maxleast  11957  minmax  11974  xrmaxleim  11988  xrmaxiflemval  11994  xrmaxlesup  12003  xrminmax  12009  summodclem3  12125  zeo3  12613  odd2np1  12618  mod2eq1n2dvds  12624  ndvdsadd  12676  fldivndvdslt  12682  bitsfval  12687  bitsval  12688  bits0  12693  bitsp1  12696  bitsmod  12701  bitscmp  12703  bitsinv1lem  12706  gcdneg  12737  nninfctlemfo  12795  algcvgblem  12805  lcmneg  12830  isprm3  12874  dvdsnprmd  12881  isprm5lem  12897  isprm5  12898  rpexp  12909  pw2dvdslemn  12921  pw2dvdseu  12924  oddpwdclemxy  12925  oddpwdclemdc  12929  oddpwdc  12930  sqpweven  12931  2sqpwodd  12932  sqne2sq  12933  phiprmpw  12978  m1dvdsndvds  13005  pythagtrip  13040  pcgcd1  13085  prmpwdvds  13112  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemodife  13218  ballotfilem4  13219  ballotfilem7  13257  oddennn  13261  ctinfomlemom  13296  ctinfom  13297  isnsgrp  13698  nzrunit  14468  opprdrng  14593  bdxmet  15525  dedekindeulemlu  15645  suplociccex  15649  dedekindicclemlu  15654  efle  15800  logleb  15899  cxple  15942  cxple3  15946  lgsmod  16059  lgsdir2lem2  16062  lgsdir2  16066  lgsne0  16071  lgsprme0  16075  lgsquadlem1  16110  2lgslem3  16134  2lgsoddprm  16146  vtxd0nedgbfi  16454  1hevtxdg0fi  16462  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  eupth2lemsfi  16633  eupth2fi  16634  konigsberglem4  16646  decidi  16737  uzdcinzz  16740  bj-charfunbi  16751  bj-nalset  16835  bj-nnelirr  16893  subctctexmid  16944  exmidnotnotr  16949  exmidcon  16950  nninfsellemeq  16962  ismkvnnlem  17007