Metamath Proof Explorer


Theorem nsstr

Description: If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion nsstr ( ( ¬ 𝐴𝐵𝐶𝐵 ) → ¬ 𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 sstr ( ( 𝐴𝐶𝐶𝐵 ) → 𝐴𝐵 )
2 1 ancoms ( ( 𝐶𝐵𝐴𝐶 ) → 𝐴𝐵 )
3 2 adantll ( ( ( ¬ 𝐴𝐵𝐶𝐵 ) ∧ 𝐴𝐶 ) → 𝐴𝐵 )
4 simpll ( ( ( ¬ 𝐴𝐵𝐶𝐵 ) ∧ 𝐴𝐶 ) → ¬ 𝐴𝐵 )
5 3 4 pm2.65da ( ( ¬ 𝐴𝐵𝐶𝐵 ) → ¬ 𝐴𝐶 )