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  890  3anor  981  nannan  1337  nannot  1339  nanbi  1340  truxortru  1415  truxorfal  1416  falxorfal  1418  nic-mpALT  1479  nic-axALT  1481  sban  2091  sbex  2176  necon3abii  2632  ne3anior  2719  inssdif0  3767  dtruALT  4545  dtruALT2  4557  dm0rn0  5077  brprcneu  5705  pmltpc  20956  cvbr2  25709  soseq  27737  brsset  27942  brtxpsd  27947  dffun10  27967  dfint3  28005  brub  28007  wl-nfeqfb  28392  frgrancvvdeqlem2  30650  pgrpgt2nabel  30799  lmod1zrnlvec  31033  bnj1143  31880  lcvbr2  32763  atlrelat1  33062