Metamath Proof Explorer


Theorem disjssi

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

Ref Expression
Hypothesis disjssi.1 𝐴𝐵
Assertion disjssi ( Disj 𝐵 → Disj 𝐴 )

Proof

Step Hyp Ref Expression
1 disjssi.1 𝐴𝐵
2 disjss ( 𝐴𝐵 → ( Disj 𝐵 → Disj 𝐴 ) )
3 1 2 ax-mp ( Disj 𝐵 → Disj 𝐴 )