Theorem sstrdi 3169

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sstrdi.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sstrdi.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
sstrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrdi

Step	Hyp	Ref	Expression
1		sstrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sstrdi.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	1, 3	sstrd 3167	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  difss2  3265  sstpr  3759  rintm  3981  eqbrrdva  4799  dmxpss2  5063  rnxpss2  5064  ssxpbm  5066  ssxp1  5067  ssxp2  5068  relfld  5159  funssxp  5387  dff2  5662  fliftf  5802  1stcof  6166  2ndcof  6167  tfrlemibfn  6331  tfr1onlembfn  6347  tfrcllemssrecs  6355  tfrcllembfn  6360  sucinc2  6449  peano5nnnn  7893  peano5nni  8924  suprzclex  9353  ioodisj  9995  fzssnn  10070  fzossnn0  10177  elfzom1elp1fzo  10204  frecuzrdgtcl  10414  frecuzrdgdomlem  10419  frecuzrdgfunlem  10421  zfz1iso  10823  seq3coll  10824  summodclem2a  11391  summodclem2  11392  zsumdc  11394  fsumsersdc  11405  fsum3cvg3  11406  prodmodclem2a  11586  prodmodclem2  11587  zproddc  11589  exmidunben  12429  nninfdclemp1  12453  strsetsid  12497  reldvdsrsrg  13266  lmss  13831  dvbssntrcntop  14238  dvcjbr  14257  reeff1olem  14277  peano5set  14777