Theorem sstrd 2070

Description: Subclass transitivity deduction.

Hypotheses

Ref	Expression
sstrd.1	|- (ph -> A (_ B)
sstrd.2	|- (ph -> B (_ C)

Assertion

Ref	Expression
sstrd	|- (ph -> A (_ C)

Proof of Theorem sstrd

Step	Hyp	Ref	Expression
1		sstr 2068	. 2 |- ((A (_ B /\ B (_ C) -> A (_ C)
2		sstrd.1	. 2 |- (ph -> A (_ B)
3		sstrd.2	. 2 |- (ph -> B (_ C)
4	1, 2, 3	sylanc 471	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   (_ wss 2043

This theorem is referenced by:  sylan9ss 2071  sspr 2471  ssxpr 3467  relfld 3507  fimacnv 3801  1stcof 4091  omwordri 4193  oewordri 4209  sbthlem1 4433  ioossre 6336  fsum1ps 6964  neiss 7673  lpss 7696  bcthlem18 7966  nmoxr 8374  nmolb 8379  nmoubi 8380  ubthlem6 8478  shintcl 9231  shub1t 9290  nmopxrt 9733  nmfnxrt 9746  nmoplbt 9771  nmopubt 9772  nmfnlbt 9787  nmfnleubt 9788  nmopunt 9877  branmfnt 9976  ssmd2 10176  mdslmd1lem1 10189  mdexch 10199  irredlem1 10254  mdsymlem5 10271  sumdmdi 10278  sumdmdlem2 10282  fgsb2 10485

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain