Metamath Proof Explorer


Theorem disjssd

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

Ref Expression
Hypothesis disjssd.1 φ A B
Assertion disjssd φ Disj B Disj A

Proof

Step Hyp Ref Expression
1 disjssd.1 φ A B
2 disjss A B Disj B Disj A
3 1 2 syl φ Disj B Disj A