Metamath Proof Explorer

Theorem disjssd

Description: Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021)

Ref Expression
Hypothesis disjssd.1 
|- ( ph -> A C_ B )
Assertion disjssd 
|- ( ph -> ( Disj B -> Disj A ) )

Proof

Step Hyp Ref Expression
1 disjssd.1 
 |-  ( ph -> A C_ B )
2 disjss 
 |-  ( A C_ B -> ( Disj B -> Disj A ) )
3 1 2 syl 
 |-  ( ph -> ( Disj B -> Disj A ) )