Theorem xchbinxr 311

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 202	. 2 |- ( ps <-> ch )
4	1, 3	xchbinx 310	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:  3anor  976  nanbi  1335  2nalexn  1624  2exnaln  1625  sbn  2088  ralnex  2723  rexnal  2724  nss  3411  difdif  3479  difab  3616  sbcnel12g  3675  ssdif0  3734  difin0ss  3742  disjsn  3933  iundif2  4234  iindif2  4236  notzfaus  4464  rexxfr  4509  nssss  4545  reldm0  5053  domtriord  7453  rnelfmlem  19425  dchrfi  22537  brsymdif  27772  df3nandALT2  28157  dvasin  28389  wopprc  29288  wwlknext  30265  lcvbr3  32356  cvrval2  32607