Metamath Proof Explorer


Theorem ssbr

Description: Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019)

Ref Expression
Assertion ssbr ⊢ A ⊆ B → C A D → C B D

Proof

Step Hyp Ref Expression
1 id ⊢ A ⊆ B → A ⊆ B
2 1 ssbrd ⊢ A ⊆ B → C A D → C B D