Theorem xchbinxr 312

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 205	. 2 |- ( ps <-> ch )
4	1, 3	xchbinx 311	1 |- ( ph <-> -. ch )

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

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 188

This theorem is referenced by:  3anor  998  nanbiOLDOLD  1390  2nalexn  1694  2exnaln  1695  sbn  2190  ralnex  2805  rexanali  2811  r2exlem  2881  nss  3458  difdif  3527  difab  3678  sbcnel12g  3740  ssdif0  3789  difin0ss  3799  disjsn  3996  iundif2  4302  iindif2  4304  brsymdif  4416  notzfaus  4535  rexxfr  4577  nssss  4613  reldm0  5007  domtriord  7664  rnelfmlem  20902  dchrfi  24118  wwlknext  25387  df3nandALT2  31000  poimirlem1  31842  dvasin  31929  lcvbr3  32495  cvrval2  32746  wopprc  35792  dfss6  36270