Theorem ssbrd

Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004)

	Ref	Expression
Hypothesis	ssbrd.1	|- ( ph -> A C_ B )
Assertion	ssbrd	|- ( ph -> ( C A D -> C B D ) )

Proof

Step	Hyp	Ref	Expression
1		ssbrd.1	|- ( ph -> A C_ B )
2	1	sseld	|- ( ph -> ( <. C , D >. e. A -> <. C , D >. e. B ) )
3		df-br	|- ( C A D <-> <. C , D >. e. A )
4		df-br	|- ( C B D <-> <. C , D >. e. B )
5	2 3 4	3imtr4g	|- ( ph -> ( C A D -> C B D ) )