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  989  nanbi  1350  2nalexn  1629  2exnaln  1630  sbn  2105  ralnex  2910  rexnalOLD  2913  rexanali  2917  r2exlem  2982  nss  3562  difdif  3630  difab  3767  sbcnel12g  3826  ssdif0  3885  difin0ss  3893  disjsn  4088  iundif2  4392  iindif2  4394  notzfaus  4622  rexxfr  4667  nssss  4703  reldm0  5220  domtriord  7663  rnelfmlem  20216  dchrfi  23286  wwlknext  24428  brsymdif  29083  df3nandALT2  29468  dvasin  29708  wopprc  30604  lcvbr3  33838  cvrval2  34089