New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  xchbinx GIF version

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
StepHypRef Expression
1 xchbinx.1 . 2 (φ ↔ ¬ ψ)
2 xchbinx.2 . . 3 (ψχ)
32notbii 287 . 2 ψ ↔ ¬ χ)
41, 3bitri 240 1 (φ ↔ ¬ χ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ 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:  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
 Copyright terms: Public domain W3C validator