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  1696  2exnaln  1697  sbn  2186  ralnex  2878  rexnalOLD  2881  rexanali  2885  r2exlem  2955  nss  3528  difdif  3597  difab  3748  sbcnel12g  3808  ssdif0  3857  difin0ss  3867  disjsn  4063  iundif2  4369  iindif2  4371  brsymdif  4482  notzfaus  4600  rexxfr  4642  nssss  4678  reldm0  5072  domtriord  7724  rnelfmlem  20898  dchrfi  24046  wwlknext  25297  df3nandALT2  30843  poimirlem1  31645  dvasin  31732  lcvbr3  32298  cvrval2  32549  wopprc  35591  dfss6  36000