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  822  dcbid  828  con1biidc  867  pm4.54dc  892  xorbi2d  1370  xorbi1d  1371  pm5.18im  1375  pm5.24dc  1388  neeq1  2348  neeq2  2349  necon3abid  2374  neleq1  2434  neleq2  2435  cdeqnot  2938  ru  2949  sbcng  2990  sbcnel12g  3061  sbcne12g  3062  difjust  3116  eldif  3124  dfdif3  3231  difeq2  3233  disjne  3461  eldifpr  3602  eldiftp  3621  prel12  3750  nalset  4111  pwnss  4137  poeq1  4276  pocl  4280  swopo  4283  sotritrieq  4302  tz7.2  4331  regexmidlem1  4509  regexmid  4511  nordeq  4520  nlimsucg  4542  nndceq0  4594  nnregexmid  4597  poinxp  4672  posng  4675  intirr  4989  poirr2  4995  cnvpom  5145  fndmdif  5589  isopolem  5789  canth  5795  poxp  6196  nnmword  6482  brdifun  6524  swoer  6525  2dom  6767  php5  6820  php5dom  6825  findcard2s  6852  fimax2gtrilemstep  6862  fimax2gtri  6863  fidcenumlemrk  6915  supeq3  6951  supeq123d  6952  supmoti  6954  eqsupti  6957  supubti  6960  supsnti  6966  isotilem  6967  isoti  6968  supisolem  6969  supisoex  6970  cnvinfex  6979  cnvti  6980  eqinfti  6981  infvalti  6983  difinfsn  7061  ismkv  7113  ismkvnex  7115  mkvprop  7118  fodjumkvlemres  7119  enmkvlem  7121  onntri35  7189  onntri45  7193  pitric  7258  addnidpig  7273  ltsonq  7335  elinp  7411  prltlu  7424  prdisj  7429  ltexprlemdisj  7543  suplocexpr  7662  ltposr  7700  aptisr  7716  suplocsrlem  7745  axpre-ltirr  7819  axpre-apti  7822  axpre-suploclemres  7838  axpre-suploc  7839  xrlenlt  7959  axapti  7965  axsuploc  7967  lttri3  7974  ltne  7979  leadd1  8324  reapti  8473  lemul1  8487  apirr  8499  apti  8516  apcon4bid  8518  lediv1  8760  lemuldiv  8772  lerec  8775  le2msq  8792  suprnubex  8844  suprleubex  8845  avgle1  9093  avgle2  9094  znnnlt1  9235  supinfneg  9529  infsupneg  9530  infregelbex  9532  eluzdc  9544  qapne  9573  xrltne  9745  xleneg  9769  nn0disj  10069  elfzonelfzo  10161  fvinim0ffz  10172  ioo0  10191  ico0  10193  ioc0  10194  flqlt  10214  expeq0  10482  nn0leexp2  10620  leisorel  10746  maxleim  11143  maxabslemval  11146  maxleast  11151  minmax  11167  xrmaxleim  11181  xrmaxiflemval  11187  xrmaxlesup  11196  xrminmax  11202  summodclem3  11317  zeo3  11801  odd2np1  11806  mod2eq1n2dvds  11812  ndvdsadd  11864  fldivndvdslt  11868  zsupcllemstep  11874  zsupcllemex  11875  zsupssdc  11883  gcdneg  11911  algcvgblem  11977  lcmneg  12002  isprm3  12046  dvdsnprmd  12053  isprm5lem  12069  isprm5  12070  rpexp  12081  pw2dvdslemn  12093  pw2dvdseu  12096  oddpwdclemxy  12097  oddpwdclemdc  12101  oddpwdc  12102  sqpweven  12103  2sqpwodd  12104  sqne2sq  12105  phiprmpw  12150  m1dvdsndvds  12176  pythagtrip  12211  pcgcd1  12255  prmpwdvds  12281  oddennn  12321  ctinfomlemom  12356  ctinfom  12357  bdxmet  13101  dedekindeulemlu  13199  suplociccex  13203  dedekindicclemlu  13208  efle  13297  logleb  13396  cxple  13437  cxple3  13441  lgsmod  13527  lgsdir2lem2  13530  lgsdir2  13534  lgsne0  13539  lgsprme0  13543  decidi  13636  uzdcinzz  13639  bj-charfunbi  13653  bj-nalset  13737  bj-nnelirr  13795  subctctexmid  13841  nninfsellemeq  13854  ismkvnnlem  13891