Theorem ssbrd 4463

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

Hypothesis

Ref	Expression
ssbrd.1	|- ( ph -> A C_ B )

Assertion

Ref	Expression
ssbrd	|- ( ph -> ( C A D -> C B D ) )

Proof of Theorem ssbrd

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

Syntax hints:   -> wi 4   e. wcel 1869   C_ wss 3437   <.cop 4003   class class class wbr 4421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3444  df-ss 3451  df-br 4422

This theorem is referenced by:  ssbri  4464  sess1  4819  brrelex12  4889  coss1  5007  coss2  5008  eqbrrdva  5021  ersym  7381  ertr  7384  fpwwe2lem6  9062  fpwwe2lem7  9063  fpwwe2lem9  9065  fpwwe2lem12  9068  fpwwe2lem13  9069  fpwwe2  9070  coss12d  13030  fthres2  15830  invfuc  15872  pospo  16212  dirref  16474  efgcpbl  17399  frgpuplem  17415  subrguss  18016  znleval  19117  ustref  21225  ustuqtop4  21251  isucn2  21286  brelg  28213  metider  28699  mclsppslem  30223  fundmpss  30408  iunrelexpuztr  36215  frege96d  36245  frege91d  36247  frege98d  36249  frege124d  36257