Theorem xchbinxr 317

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)

Hypotheses

Ref	Expression
xchbinxr.1	|- ( ph <-> -. ps )
xchbinxr.2	|- ( ch <-> ps )

Assertion

Ref	Expression
xchbinxr	|- ( ph <-> -. ch )

Proof of Theorem xchbinxr

Step	Hyp	Ref	Expression
1		xchbinxr.1	. 2 |- ( ph <-> -. ps )
2		xchbinxr.2	. . 3 |- ( ch <-> ps )
3	2	bicomi 207	. 2 |- ( ps <-> ch )
4	1, 3	xchbinx 316	1 |- ( ph <-> -. ch )

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

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 190

This theorem is referenced by:  3anor  1007  nanbiOLDOLD  1405  2nalexn  1711  2exnaln  1712  sbn  2231  ralnex  2846  rexanali  2852  r2exlem  2922  nss  3502  difdif  3571  difab  3724  sbcnel12g  3786  ssdif0  3835  difin0ss  3845  disjsn  4044  iundif2  4359  iindif2  4361  brsymdif  4473  notzfaus  4592  rexxfr  4634  nssss  4670  reldm0  5071  domtriord  7744  rnelfmlem  21016  dchrfi  24232  wwlknext  25501  df3nandALT2  31107  bj-ssbn  31299  poimirlem1  31986  dvasin  32073  lcvbr3  32634  cvrval2  32885  wopprc  35930  dfss6  36408