Theorem unssad 4143

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3900   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919

This theorem is referenced by:  naddcllem  8591  ersym  8634  findcard2d  9076  finsschain  9243  r0weon  9900  ackbij1lem16  10122  wunex2  10626  sumsplit  15672  fsumabs  15705  fsumiun  15725  mrieqvlemd  17532  yonedalem1  18175  yonedalem21  18176  yonedalem22  18181  yonffthlem  18185  lsmsp  21018  mplcoe1  21970  mdetunilem9  22533  ordtbas  23105  isufil2  23821  ufileu  23832  filufint  23833  fmfnfm  23871  flimclslem  23897  fclsfnflim  23940  flimfnfcls  23941  imasdsf1olem  24286  limcdif  25802  jensenlem1  26922  jensenlem2  26923  jensen  26924  gsumvsca1  33190  gsumvsca2  33191  qsdrngilem  33454  fldgenfldext  33676  evls1fldgencl  33678  fldextrspunlem1  33683  fldextrspunfld  33684  algextdeglem1  33725  algextdeglem2  33726  algextdeglem3  33727  algextdeglem4  33728  constrextdg2lem  33756  constrllcllem  33760  constrlccllem  33761  constrcccllem  33762  ordtconnlem1  33932  ssmcls  35599  mclsppslem  35615  rngunsnply  43201  mptrcllem  43645  clcnvlem  43655  brtrclfv2  43759  isotone1  44080  dvnprodlem1  45983