This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xchbinxr

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014)

Ref Expression
Hypotheses xchbinxr.1 ⊢ φ ↔ ¬ ψ
xchbinxr.2 ⊢ χ ↔ ψ
Assertion xchbinxr ⊢ φ ↔ ¬ χ

Proof

Step Hyp Ref Expression
1 xchbinxr.1 ⊢ φ ↔ ¬ ψ
2 xchbinxr.2 ⊢ χ ↔ ψ
3 2 bicomi ⊢ ψ ↔ χ
4 1 3 xchbinx ⊢ φ ↔ ¬ χ