Theorem xchbinx 301

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)

Hypotheses

Ref	Expression
xchbinx.1	|- (ph <-> -. ps)
xchbinx.2	|- (ps <-> ch)

Assertion

Ref	Expression
xchbinx	|- (ph <-> -. ch)

Proof of Theorem xchbinx

Step	Hyp	Ref	Expression
1		xchbinx.1	. 2 |- (ph <-> -. ps)
2		xchbinx.2	. . 3 |- (ps <-> ch)
3	2	notbii 287	. 2 |- (-. ps <-> -. ch)
4	1, 3	bitri 240	1 |- (ph <-> -. ch)

Syntax hints:  -. wn 3   <-> 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:  xchbinxr  302  con1bii  321  pm4.52  477  pm4.54  479  xordi  865  3anor  948  nannan  1291  nannot  1293  nanbi  1294  truxortru  1358  truxorfal  1359  falxorfal  1361  nic-mpALT  1437  nic-axALT  1439  sban  2069  sbex  2128  necon3abii  2547  ne3anior  2603  elcomplg  3219  inssdif0  3618  dfimak2  4299  nnsucelrlem3  4427  nndisjeq  4430  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlower  4484  eqtfinrelk  4487  nnadjoinlem1  4520  nnadjoinpw  4522  sfindbl  4531  setconslem2  4733  setconslem3  4734  dm0rn0  4922  brimage  5794  releqel  5808  releqmpt2  5810  fnfullfunlem1  5857  refex  5912  extex  5916  nenpw1pwlem1  6085  ovcelem1  6172  tcfnex  6245  nchoicelem10  6299