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 
|- ( ( -. A C_ B /\ C C_ B ) -> -. A C_ C )

Proof

Step Hyp Ref Expression
1 sstr 
 |-  ( ( A C_ C /\ C C_ B ) -> A C_ B )
2 1 ancoms 
 |-  ( ( C C_ B /\ A C_ C ) -> A C_ B )
3 2 adantll 
 |-  ( ( ( -. A C_ B /\ C C_ B ) /\ A C_ C ) -> A C_ B )
4 simpll 
 |-  ( ( ( -. A C_ B /\ C C_ B ) /\ A C_ C ) -> -. A C_ B )
5 3 4 pm2.65da 
 |-  ( ( -. A C_ B /\ C C_ B ) -> -. A C_ C )