This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssbrd

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

		Ref	Expression
	Hypothesis	ssbrd.1	$⊢ φ \to A \subseteq B$
	Assertion	ssbrd	$⊢ φ \to (C A D \to C B D)$

Step	Hyp	Ref	Expression
1		ssbrd.1	$⊢ φ \to A \subseteq B$
2	1	sseld	$⊢ φ \to (⟨C, D⟩ \in A \to ⟨C, D⟩ \in B)$
3		df-br	$⊢ C A D \leftrightarrow ⟨C, D⟩ \in A$
4		df-br	$⊢ C B D \leftrightarrow ⟨C, D⟩ \in B$
5	2 3 4	3imtr4g	$⊢ φ \to (C A D \to C B D)$