Theorem notbid 625

Description: Deduction negating both sides of a logical equivalence. (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	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	biimprd 156	. . 3 |- ( ph -> ( ch -> ps ) )
3	2	con3d 594	. 2 |- ( ph -> ( -. ps -> -. ch ) )
4	1	biimpd 142	. . 3 |- ( ph -> ( ps -> ch ) )
5	4	con3d 594	. 2 |- ( ph -> ( -. ch -> -. ps ) )
6	3, 5	impbid 127	1 |- ( ph -> ( -. ps <-> -. ch ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  notbii  627  stbid  775  dcbid  784  con1biidc  807  pm4.54dc  841  xorbi2d  1314  xorbi1d  1315  pm5.18im  1319  pm5.24dc  1332  neeq1  2264  neeq2  2265  necon3abid  2290  neleq1  2350  neleq2  2351  cdeqnot  2816  ru  2827  sbcng  2867  sbcnel12g  2936  sbcne12g  2937  difjust  2987  eldif  2995  dfdif3  3096  difeq2  3098  disjne  3321  ifbi  3394  prel12  3592  nalset  3937  pwnss  3962  poeq1  4093  pocl  4097  swopo  4100  sotritrieq  4119  tz7.2  4148  regexmidlem1  4315  regexmid  4317  nordeq  4326  nlimsucg  4348  nndceq0  4397  nnregexmid  4400  poinxp  4468  posng  4471  intirr  4776  poirr2  4782  cnvpom  4930  fndmdif  5352  isopolem  5543  poxp  5935  nnmword  6210  brdifun  6252  swoer  6253  2dom  6455  php5  6507  php5dom  6512  findcard2s  6539  supeq3  6606  supeq123d  6607  supmoti  6609  eqsupti  6612  supubti  6615  supsnti  6621  isotilem  6622  isoti  6623  supisolem  6624  supisoex  6625  cnvinfex  6634  cnvti  6635  eqinfti  6636  infvalti  6638  pitric  6801  addnidpig  6816  ltsonq  6878  elinp  6954  prltlu  6967  prdisj  6972  ltexprlemdisj  7086  ltposr  7230  aptisr  7245  axpre-ltirr  7338  axpre-apti  7341  xrlenlt  7472  axapti  7478  lttri3  7486  ltne  7491  leadd1  7829  reapti  7974  lemul1  7988  apirr  8000  apti  8017  lediv1  8242  lemuldiv  8254  lerec  8257  le2msq  8274  suprnubex  8326  suprleubex  8327  avgle1  8566  avgle2  8567  znnnlt1  8708  supinfneg  8992  infsupneg  8993  eluzdc  9006  qapne  9033  xrltne  9187  xleneg  9208  nn0disj  9453  elfzonelfzo  9544  fvinim0ffz  9555  ioo0  9574  ico0  9576  ioc0  9577  flqlt  9593  expeq0  9837  abs00  10338  maxleim  10479  maxabslemval  10482  maxleast  10487  minmax  10500  zeo3  10662  odd2np1  10667  mod2eq1n2dvds  10673  ndvdsadd  10725  fldivndvdslt  10729  zsupcllemstep  10735  zsupcllemex  10736  gcdneg  10767  algcvgblem  10825  lcmneg  10850  isprm3  10894  dvdsnprmd  10901  rpexp  10926  pw2dvdslemn  10937  pw2dvdseu  10940  oddpwdclemxy  10941  oddpwdclemdc  10945  oddpwdc  10946  sqpweven  10947  2sqpwodd  10948  sqne2sq  10949  phiprmpw  10992  oddennn  10999  decidi  11052  uzdcinzz  11055  bj-nalset  11143  bj-nnelirr  11205  nninfsellemeq  11262