MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssbri Structured version   Unicode version

Theorem ssbri 4484
Description: Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
Hypothesis
Ref Expression
ssbri.1  |-  A  C_  B
Assertion
Ref Expression
ssbri  |-  ( C A D  ->  C B D )

Proof of Theorem ssbri
StepHypRef Expression
1 ssbri.1 . . . 4  |-  A  C_  B
21a1i 11 . . 3  |-  ( T. 
->  A  C_  B )
32ssbrd 4483 . 2  |-  ( T. 
->  ( C A D  ->  C B D ) )
43trud 1383 1  |-  ( C A D  ->  C B D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   T. wtru 1375    C_ wss 3471   class class class wbr 4442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3478  df-ss 3485  df-br 4443
This theorem is referenced by:  brel  5042  swoer  7331  swoord1  7332  swoord2  7333  ecopover  7407  endom  7534  brdom3  8897  brdom5  8898  brdom4  8899  fpwwe2lem13  9011  nqerf  9299  nqerrel  9301  isfull  15128  isfth  15132  fulloppc  15140  fthoppc  15141  fthsect  15143  fthinv  15144  fthmon  15145  fthepi  15146  ffthiso  15147  catcisolem  15282  psss  15692  efgrelex  16560  hlimadd  25774  hhsscms  25859  occllem  25885  nlelchi  26644  hmopidmchi  26734  fundmpss  28761  itg2gt0cn  29636  fnessref  29754  brresi  29801
  Copyright terms: Public domain W3C validator