Theorem notbid 285

Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)

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	. . 3 |- (ph -> (ps <-> ch))
2		notnot 282	. . 3 |- (ps <-> -. -. ps)
3		notnot 282	. . 3 |- (ch <-> -. -. ch)
4	1, 2, 3	3bitr3g 278	. 2 |- (ph -> (-. -. ps <-> -. -. ch))
5	4	con4bid 284	1 |- (ph -> (-. ps <-> -. ch))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  notbi  286  con3th  924  nanbi1  1295  xorbi12d  1315  cbvexvw  1703  hba1w  1707  hbe1w  1708  ax10lem2  1937  ax9  1949  equsex  1962  drex1  1967  cbvex  1985  cbvexd  2009  ax11inda  2200  eujustALT  2207  2mo  2282  neeq1  2524  neeq2  2525  necon3abid  2549  neleq1  2607  neleq2  2608  cbvrexf  2830  gencbval  2903  spcegf  2935  spc2gv  2942  spc3gv  2944  ru  3045  sbcng  3086  sbcrext  3119  sbcnel12g  3153  cbvrexcsf  3199  elin  3219  dfpss3  3355  disjne  3596  pssdifcom1  3635  pssdifcom2  3636  pw1disj  4167  opkelimagekg  4271  dfimak2  4298  nnsucelr  4428  tfinltfin  4501  tfinlefin  4502  evenodddisjlem1  4515  evenodddisj  4516  nnadjoin  4520  nnadjoinpw  4521  tfinnn  4534  nulnnn  4556  rexiunxp  4824  intirr  5029  fvun1  5379  fvmpti  5699  enadjlem1  6059  enadj  6060  nenpw1pwlem2  6085  nnc3n3p1  6278  nchoicelem1  6289  nchoicelem2  6290  nchoicelem8  6296  nchoicelem11  6299  nchoicelem16  6304