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 C_ B -> ( C A D -> C B D ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A C_ B -> A C_ B )
2 1 ssbrd 
 |-  ( A C_ B -> ( C A D -> C B D ) )