Metamath Proof Explorer


Theorem xchnxbi

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

Ref Expression
Hypotheses xchnxbi.1 ¬φψ
xchnxbi.2 φχ
Assertion xchnxbi ¬χψ

Proof

Step Hyp Ref Expression
1 xchnxbi.1 ¬φψ
2 xchnxbi.2 φχ
3 2 notbii ¬φ¬χ
4 3 1 bitr3i ¬χψ