Theorem sstrd 3165

Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)

Hypotheses

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

Assertion

Ref	Expression
sstrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrd

Step	Hyp	Ref	Expression
1		sstrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		sstr 3163	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3129

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 3135  df-ss 3142

This theorem is referenced by:  sstrid  3166  sstrdi  3167  ssdif2d  3274  tfisi  4586  funss  5235  fssxp  5383  fvmptssdm  5600  suppssfv  6078  suppssov1  6079  tposss  6246  tfrlem1  6308  tfrlemibfn  6328  tfr1onlembfn  6344  tfr1onlemubacc  6346  tfr1onlemres  6349  tfrcllembfn  6357  tfrcllemubacc  6359  tfrcllemres  6362  ecinxp  6609  undifdc  6922  sbthlem1  6955  iseqf1olemnab  10487  fiubm  10807  isumss  11398  prodssdc  11596  ennnfoneleminc  12411  strsetsid  12494  strleund  12561  strext  12563  imasaddvallemg  12735  subsubg  13055  subgintm  13056  subsubrg  13364  ntrss  13589  neiint  13615  neiss  13620  restopnb  13651  iscnp4  13688  blssps  13897  blss  13898  xmettx  13980  tgqioo  14017  rescncf  14038  suplociccreex  14072  suplociccex  14073  dvbss  14124  dvbsssg  14125  dvfgg  14127  dvcnp2cntop  14133  dvcn  14134  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141