Metamath Proof Explorer


Theorem sbcni

Description: Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

Ref Expression
Hypotheses sbcni.1 A V
sbcni.2 [˙A / x]˙ φ ψ
Assertion sbcni [˙A / x]˙ ¬ φ ¬ ψ

Proof

Step Hyp Ref Expression
1 sbcni.1 A V
2 sbcni.2 [˙A / x]˙ φ ψ
3 sbcng A V [˙A / x]˙ ¬ φ ¬ [˙A / x]˙ φ
4 1 3 ax-mp [˙A / x]˙ ¬ φ ¬ [˙A / x]˙ φ
5 4 2 xchbinx [˙A / x]˙ ¬ φ ¬ ψ