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  891  3anor  984  nannan  1342  nannot  1344  nanbi  1345  truxortru  1420  truxorfal  1421  falxorfal  1423  nic-mpALT  1484  nic-axALT  1486  sban  2107  sbex  2191  necon3abii  2720  ne3anior  2786  inssdif0  3887  dtruALT  4672  dtruALT2  4684  dm0rn0  5210  brprcneu  5850  pmltpc  21590  frgrancvvdeqlem2  24694  cvbr2  26864  soseq  28897  brsset  29102  brtxpsd  29107  dffun10  29127  dfint3  29165  brub  29167  wl-nfeqfb  29553  pgrpgt2nabl  31899  lmod1zrnlvec  32051  bnj1143  32803  lcvbr2  33694  atlrelat1  33993