Theorem xchbinx 312

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

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

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 189

This theorem is referenced by:  xchbinxr  313  con1bii  333  pm4.52  494  pm4.54  496  xordi  905  3anor  1000  nancom  1386  nannanOLD  1389  nannot  1391  nanbiOLDOLD  1394  xorneg1  1416  trunanfal  1486  truxortru  1490  truxorfal  1491  falxorfal  1494  nic-mpALT  1554  nic-axALT  1556  sban  2227  sbex  2291  necon3abii  2669  ne3anior  2716  ralnex2  2892  ralnex3  2893  inssdif0  3833  dtruALT  4631  dtruALT2  4643  dm0rn0  5050  brprcneu  5856  0nelfz1  11815  pmltpc  22394  frgrancvvdeqlem2  25752  cvbr2  27929  bnj1143  29595  soseq  30485  brsset  30649  brtxpsd  30654  dffun10  30674  dfint3  30712  brub  30714  wl-nfeqfb  31863  sbcni  32342  lcvbr2  32582  atlrelat1  32881  dfxor5  36353  df3an2  36355  falseral0  38980  nbgrnself  39412  rgrx0ndm  39591  pgrpgt2nabl  40138  lmod1zrnlvec  40274  aacllem  40527