Theorem sstrd 2074

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 2072	. 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 2047

This theorem is referenced by:  sylan9ss 2075  sspr 2475  ssxpr 3475  relfld 3515  fimacnv 3810  1stcof 4101  omwordri 4203  oewordri 4219  sbthlem1 4447  fsum1ps 7018  neiss 7723  lpss 7746  bcthlem18 8016  nmoxr 8429  nmolb 8434  nmoubi 8435  ubthlem6 8534  shintcl 9293  shub1t 9352  nmopxrt 9793  nmfnxrt 9806  nmoplbt 9831  nmopubt 9832  nmfnlbt 9848  nmfnleubt 9849  nmopunt 9939  branmfnt 10038  ssmd2 10239  mdslmd1lem1 10252  mdexch 10262  irredlem1 10317  mdsymlem5 10334  sumdmdi 10342  sumdmdlem2 10346  fgsb2 10580

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain