Theorem ssbrd 4437

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 3417	. 2 |- ( ph -> ( <. C , D >. e. A -> <. C , D >. e. B ) )
3		df-br 4396	. 2 |- ( C A D <-> <. C , D >. e. A )
4		df-br 4396	. 2 |- ( C B D <-> <. C , D >. e. B )
5	2, 3, 4	3imtr4g 278	1 |- ( ph -> ( C A D -> C B D ) )

Syntax hints:   -> wi 4   e. wcel 1904   C_ wss 3390   <.cop 3965   class class class wbr 4395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404  df-br 4396

This theorem is referenced by:  ssbri  4438  sess1  4807  brrelex12  4877  coss1  4995  coss2  4996  eqbrrdva  5009  ersym  7393  ertr  7396  fpwwe2lem6  9078  fpwwe2lem7  9079  fpwwe2lem9  9081  fpwwe2lem12  9084  fpwwe2lem13  9085  fpwwe2  9086  coss12d  13111  fthres2  15915  invfuc  15957  pospo  16297  dirref  16559  efgcpbl  17484  frgpuplem  17500  subrguss  18101  znleval  19202  ustref  21311  ustuqtop4  21337  isucn2  21372  brelg  28293  metider  28771  mclsppslem  30293  fundmpss  30478  iunrelexpuztr  36382  frege96d  36412  frege91d  36414  frege98d  36416  frege124d  36424  ssrelrn  39156