Theorem xchbinx 301

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

Hypotheses

Ref	Expression
xchbinx.1	⊢ (φ ↔ ¬ ψ)
xchbinx.2	⊢ (ψ ↔ χ)

Assertion

Ref	Expression
xchbinx	⊢ (φ ↔ ¬ χ)

Proof of Theorem xchbinx

Step	Hyp	Ref	Expression
1		xchbinx.1	. 2 ⊢ (φ ↔ ¬ ψ)
2		xchbinx.2	. . 3 ⊢ (ψ ↔ χ)
3	2	notbii 287	. 2 ⊢ (¬ ψ ↔ ¬ χ)
4	1, 3	bitri 240	1 ⊢ (φ ↔ ¬ χ)

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  2546  ne3anior  2602  elcomplg  3218  inssdif0  3617  dfimak2  4298  nnsucelrlem3  4426  nndisjeq  4429  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlower  4483  eqtfinrelk  4486  nnadjoinlem1  4519  nnadjoinpw  4521  sfindbl  4530  setconslem2  4732  setconslem3  4733  dm0rn0  4921  brimage  5793  releqel  5807  releqmpt2  5809  fnfullfunlem1  5856  refex  5911  extex  5915  nenpw1pwlem1  6084  ovcelem1  6171  tcfnex  6244  nchoicelem10  6298