Theorem unssad 4117

Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4114. Partial converse of unssd 4116. (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 4114	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 233	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  ersym  8468  findcard2d  8911  finsschain  9056  r0weon  9699  ackbij1lem16  9922  wunex2  10425  sumsplit  15408  fsumabs  15441  fsumiun  15461  mrieqvlemd  17255  yonedalem1  17906  yonedalem21  17907  yonedalem22  17912  yonffthlem  17916  lsmsp  20263  mplcoe1  21148  mdetunilem9  21677  ordtbas  22251  isufil2  22967  ufileu  22978  filufint  22979  fmfnfm  23017  flimclslem  23043  fclsfnflim  23086  flimfnfcls  23087  imasdsf1olem  23434  limcdif  24945  jensenlem1  26041  jensenlem2  26042  jensen  26043  gsumvsca1  31381  gsumvsca2  31382  ordtconnlem1  31776  ssmcls  33429  mclsppslem  33445  naddcllem  33758  rngunsnply  40914  mptrcllem  41110  clcnvlem  41120  brtrclfv2  41224  isotone1  41547  dvnprodlem1  43377