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