Theorem xchbinx 324

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 310	. 2 |- ( -. ps <-> -. ch )
4	1, 3	bitri 264	1 |- ( ph <-> -. ch )

Syntax hints:   -. wn 3   <-> wb 196

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 197

This theorem is referenced by:  xchbinxr  325  con1bii  346  pm4.52  512  pm4.54  514  xordi  937  3anor  1054  nancom  1450  nannot  1453  xorneg1  1475  trunanfal  1525  truxortru  1528  truxorfal  1529  falxorfal  1531  nic-mpALT  1597  nic-axALT  1599  sban  2399  sbex  2463  necon3abii  2840  ne3anior  2887  ralnex2  3045  ralnex3  3046  inssdif0  3947  falseral0  4081  dtruALT  4899  dtruALT2  4911  dm0rn0  5342  brprcneu  6184  0nelfz1  12360  pmltpc  23219  nbgrnself  26257  rgrx0ndm  26489  nfrgr2v  27136  frgrncvvdeqlem1  27163  cvbr2  29142  bnj1143  30861  soseq  31751  brsset  31996  brtxpsd  32001  dffun10  32021  dfint3  32059  brub  32061  wl-nfeqfb  33323  sbcni  33914  brvdif2  34026  lcvbr2  34309  atlrelat1  34608  dfxor5  38059  df3an2  38061  clsk1independent  38344  spr0nelg  41726  pgrpgt2nabl  42147  lmod1zrnlvec  42283  aacllem  42547