Metamath Proof Explorer

Theorem ssneldd

Description: If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses ssneld.1 φ A B
ssneldd.2 φ ¬ C B
Assertion ssneldd φ ¬ C A


Step Hyp Ref Expression
1 ssneld.1 φ A B
2 ssneldd.2 φ ¬ C B
3 1 ssneld φ ¬ C B ¬ C A
4 2 3 mpd φ ¬ C A