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-mp 5  ax-1 6  ax-2 7  ax-3 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  2525  neeq2  2526  necon3abid  2550  neleq1  2608  neleq2  2609  cbvrexf  2831  gencbval  2904  spcegf  2936  spc2gv  2943  spc3gv  2945  ru  3046  sbcng  3087  sbcrext  3120  sbcnel12g  3154  cbvrexcsf  3200  elin  3220  dfpss3  3356  disjne  3597  pssdifcom1  3636  pssdifcom2  3637  pw1disj  4168  opkelimagekg  4272  dfimak2  4299  nnsucelr  4429  tfinltfin  4502  tfinlefin  4503  evenodddisjlem1  4516  evenodddisj  4517  nnadjoin  4521  nnadjoinpw  4522  tfinnn  4535  nulnnn  4557  rexiunxp  4825  intirr  5030  fvun1  5380  fvmpti  5700  enadjlem1  6060  enadj  6061  nenpw1pwlem2  6086  nnc3n3p1  6279  nchoicelem1  6290  nchoicelem2  6291  nchoicelem8  6297  nchoicelem11  6300  nchoicelem16  6305