Theorem unssad 4121

Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4118. Partial converse of unssd 4120. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unssad.1	⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)

Assertion

Ref	Expression
unssad	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem unssad

Step	Hyp	Ref	Expression
1		unssad.1	. . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
2		unss 4118	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 233	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simpld 495	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∪ cun 3885   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904

This theorem is referenced by:  ersym  8510  findcard2d  8949  finsschain  9126  r0weon  9768  ackbij1lem16  9991  wunex2  10494  sumsplit  15480  fsumabs  15513  fsumiun  15533  mrieqvlemd  17338  yonedalem1  17990  yonedalem21  17991  yonedalem22  17996  yonffthlem  18000  lsmsp  20348  mplcoe1  21238  mdetunilem9  21769  ordtbas  22343  isufil2  23059  ufileu  23070  filufint  23071  fmfnfm  23109  flimclslem  23135  fclsfnflim  23178  flimfnfcls  23179  imasdsf1olem  23526  limcdif  25040  jensenlem1  26136  jensenlem2  26137  jensen  26138  gsumvsca1  31479  gsumvsca2  31480  ordtconnlem1  31874  ssmcls  33529  mclsppslem  33545  naddcllem  33831  rngunsnply  40998  mptrcllem  41221  clcnvlem  41231  brtrclfv2  41335  isotone1  41658  dvnprodlem1  43487