Theorem notbid 624

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 593	. 2 |- ( ph -> ( -. ps -> -. ch ) )
4	1	biimpd 142	. . 3 |- ( ph -> ( ps -> ch ) )
5	4	con3d 593	. 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 576  ax-in2 577

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  notbii  626  dcbid  781  con1biidc  804  pm4.54dc  838  xorbi2d  1311  xorbi1d  1312  pm5.18im  1316  pm5.24dc  1329  neeq1  2258  neeq2  2259  necon3abid  2284  neleq1  2343  neleq2  2344  cdeqnot  2803  ru  2814  sbcng  2854  sbcnel12g  2923  sbcne12g  2924  difjust  2974  eldif  2982  difeq2  3084  disjne  3297  ifbi  3369  prel12  3563  nalset  3908  pwnss  3933  poeq1  4054  pocl  4058  swopo  4061  sotritrieq  4080  tz7.2  4109  regexmidlem1  4276  regexmid  4278  nordeq  4287  nlimsucg  4309  nndceq0  4357  nnregexmid  4360  poinxp  4427  posng  4430  intirr  4731  poirr2  4737  cnvpom  4880  fndmdif  5293  isopolem  5481  poxp  5873  nnmword  6114  brdifun  6156  swoer  6157  2dom  6308  php5  6344  php5dom  6349  findcard2s  6374  supeq3  6403  supeq123d  6404  supmoti  6406  eqsupti  6409  supubti  6412  supsnti  6418  isotilem  6419  isoti  6420  supisolem  6421  supisoex  6422  cnvinfex  6431  cnvti  6432  eqinfti  6433  infvalti  6435  pitric  6511  addnidpig  6526  ltsonq  6588  elinp  6664  prltlu  6677  prdisj  6682  ltexprlemdisj  6796  ltposr  6940  aptisr  6955  axpre-ltirr  7048  axpre-apti  7051  xrlenlt  7177  axapti  7183  lttri3  7191  ltne  7196  leadd1  7534  reapti  7679  lemul1  7693  apirr  7705  apti  7722  lediv1  7947  lemuldiv  7959  lerec  7962  le2msq  7979  suprnubex  8031  suprleubex  8032  avgle1  8271  avgle2  8272  znnnlt1  8399  supinfneg  8683  infsupneg  8684  eluzdc  8697  qapne  8724  xrltne  8883  xleneg  8904  nn0disj  9148  elfzonelfzo  9239  fvinim0ffz  9250  ioo0  9268  ico0  9270  ioc0  9271  flqlt  9285  expeq0  9507  abs00  9950  maxleim  10091  maxabslemval  10094  maxleast  10099  minmax  10112  zeo3  10267  odd2np1  10272  mod2eq1n2dvds  10279  ndvdsadd  10331  fldivndvdslt  10335  zsupcllemstep  10341  zsupcllemex  10342  gcdneg  10373  algcvgblem  10431  lcmneg  10456  isprm3  10500  dvdsnprmd  10507  rpexp  10532  pw2dvdslemn  10543  pw2dvdseu  10546  oddpwdclemxy  10547  oddpwdclemdc  10551  oddpwdc  10552  sqpweven  10553  2sqpwodd  10554  sqne2sq  10555  bj-nalset  10686  bj-nnelirr  10748