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  981  nanbi  1341  2nalexn  1620  2exnaln  1621  sbn  2091  ralnex  2848  rexnalOLD  2850  nss  3517  difdif  3585  difab  3722  sbcnel12g  3781  ssdif0  3840  difin0ss  3848  disjsn  4039  iundif2  4340  iindif2  4342  notzfaus  4570  rexxfr  4615  nssss  4651  reldm0  5160  domtriord  7562  rnelfmlem  19652  dchrfi  22722  brsymdif  27998  df3nandALT2  28383  dvasin  28623  wopprc  29522  wwlknext  30499  lcvbr3  32987  cvrval2  33238