Theorem xchbinx 302

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

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

This theorem is referenced by:  xchbinxr  303  con1bii  322  pm4.52  478  pm4.54  480  xordi  866  3anor  950  nannan  1297  nannot  1299  nanbi  1300  truxortru  1364  truxorfal  1365  falxorfal  1367  nic-mpALT  1443  nic-axALT  1445  sban  2118  sbex  2178  necon3abii  2597  ne3anior  2653  inssdif0  3655  dtruALT  4356  dtruALT2  4368  dm0rn0  5045  brprcneu  5680  pmltpc  19300  cvbr2  23739  soseq  25468  brsset  25643  brtxpsd  25648  frgrancvvdeqlem2  28134  bnj1143  28867  sbanNEW7  29273  sbexNEW7  29318  lcvbr2  29505  atlrelat1  29804

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 178