Theorem xchbinx 311

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

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

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 188

This theorem is referenced by:  xchbinxr  312  con1bii  332  pm4.52  493  pm4.54  495  xordi  903  3anor  998  nancom  1382  nannanOLD  1385  nannot  1387  nanbiOLDOLD  1390  xorneg1  1412  trunanfal  1482  truxortru  1486  truxorfal  1487  falxorfal  1490  nic-mpALT  1551  nic-axALT  1553  sban  2191  sbex  2256  necon3abii  2682  ne3anior  2748  ralnex2  2929  ralnex3  2930  inssdif0  3859  dtruALT  4645  dtruALT2  4657  dm0rn0  5062  brprcneu  5865  0nelfz1  11805  pmltpc  22308  frgrancvvdeqlem2  25645  cvbr2  27812  bnj1143  29431  soseq  30320  brsset  30482  brtxpsd  30487  dffun10  30507  dfint3  30545  brub  30547  wl-nfeqfb  31618  sbcni  32097  lcvbr2  32341  atlrelat1  32640  dfxor5  36046  pgrpgt2nabl  38968  lmod1zrnlvec  39104  aacllem  39358