Theorem xchbinx 310

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

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

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 185

This theorem is referenced by:  xchbinxr  311  con1bii  331  pm4.52  491  pm4.54  493  xordi  893  3anor  988  nancom  1345  nannanOLD  1348  nannot  1350  nanbiOLD  1352  truxortru  1427  truxorfal  1428  falxorfal  1430  nic-mpALT  1490  nic-axALT  1492  sban  2124  sbex  2191  necon3abii  2701  ne3anior  2767  inssdif0  3877  dtruALT  4665  dtruALT2  4677  dm0rn0  5205  brprcneu  5845  pmltpc  21728  frgrancvvdeqlem2  24896  cvbr2  27067  soseq  29302  brsset  29507  brtxpsd  29512  dffun10  29532  dfint3  29570  brub  29572  wl-nfeqfb  29958  sbcni  30482  ralnex2  31385  pgrpgt2nabl  32667  lmod1zrnlvec  32805  bnj1143  33556  lcvbr2  34449  atlrelat1  34748