Theorem notbid 656

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 655	. 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 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  stbid  817  dcbid  823  con1biidc  862  pm4.54dc  887  xorbi2d  1358  xorbi1d  1359  pm5.18im  1363  pm5.24dc  1376  neeq1  2321  neeq2  2322  necon3abid  2347  neleq1  2407  neleq2  2408  cdeqnot  2897  ru  2908  sbcng  2949  sbcnel12g  3019  sbcne12g  3020  difjust  3072  eldif  3080  dfdif3  3186  difeq2  3188  disjne  3416  prel12  3698  nalset  4058  pwnss  4083  poeq1  4221  pocl  4225  swopo  4228  sotritrieq  4247  tz7.2  4276  regexmidlem1  4448  regexmid  4450  nordeq  4459  nlimsucg  4481  nndceq0  4531  nnregexmid  4534  poinxp  4608  posng  4611  intirr  4925  poirr2  4931  cnvpom  5081  fndmdif  5525  isopolem  5723  poxp  6129  nnmword  6414  brdifun  6456  swoer  6457  2dom  6699  php5  6752  php5dom  6757  findcard2s  6784  fimax2gtrilemstep  6794  fimax2gtri  6795  fidcenumlemrk  6842  supeq3  6877  supeq123d  6878  supmoti  6880  eqsupti  6883  supubti  6886  supsnti  6892  isotilem  6893  isoti  6894  supisolem  6895  supisoex  6896  cnvinfex  6905  cnvti  6906  eqinfti  6907  infvalti  6909  difinfsn  6985  ismkv  7027  ismkvnex  7029  mkvprop  7032  fodjumkvlemres  7033  pitric  7129  addnidpig  7144  ltsonq  7206  elinp  7282  prltlu  7295  prdisj  7300  ltexprlemdisj  7414  suplocexpr  7533  ltposr  7571  aptisr  7587  suplocsrlem  7616  axpre-ltirr  7690  axpre-apti  7693  axpre-suploclemres  7709  axpre-suploc  7710  xrlenlt  7829  axapti  7835  axsuploc  7837  lttri3  7844  ltne  7849  leadd1  8192  reapti  8341  lemul1  8355  apirr  8367  apti  8384  apcon4bid  8386  lediv1  8627  lemuldiv  8639  lerec  8642  le2msq  8659  suprnubex  8711  suprleubex  8712  avgle1  8960  avgle2  8961  znnnlt1  9102  supinfneg  9390  infsupneg  9391  eluzdc  9404  qapne  9431  xrltne  9596  xleneg  9620  nn0disj  9915  elfzonelfzo  10007  fvinim0ffz  10018  ioo0  10037  ico0  10039  ioc0  10040  flqlt  10056  expeq0  10324  leisorel  10580  maxleim  10977  maxabslemval  10980  maxleast  10985  minmax  11001  xrmaxleim  11013  xrmaxiflemval  11019  xrmaxlesup  11028  xrminmax  11034  summodclem3  11149  zeo3  11565  odd2np1  11570  mod2eq1n2dvds  11576  ndvdsadd  11628  fldivndvdslt  11632  zsupcllemstep  11638  zsupcllemex  11639  gcdneg  11670  algcvgblem  11730  lcmneg  11755  isprm3  11799  dvdsnprmd  11806  rpexp  11831  pw2dvdslemn  11843  pw2dvdseu  11846  oddpwdclemxy  11847  oddpwdclemdc  11851  oddpwdc  11852  sqpweven  11853  2sqpwodd  11854  sqne2sq  11855  phiprmpw  11898  oddennn  11905  ctinfomlemom  11940  ctinfom  11941  bdxmet  12670  dedekindeulemlu  12768  suplociccex  12772  dedekindicclemlu  12777  decidi  13002  uzdcinzz  13005  bj-nalset  13093  bj-nnelirr  13151  subctctexmid  13196  nninfsellemeq  13210