Theorem unssad 4145

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3899   ⊆ wss 3901

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  naddcllem  8604  ersym  8647  findcard2d  9091  finsschain  9259  r0weon  9922  ackbij1lem16  10144  wunex2  10649  sumsplit  15691  fsumabs  15724  fsumiun  15744  mrieqvlemd  17552  yonedalem1  18195  yonedalem21  18196  yonedalem22  18201  yonffthlem  18205  lsmsp  21038  mplcoe1  21992  mdetunilem9  22564  ordtbas  23136  isufil2  23852  ufileu  23863  filufint  23864  fmfnfm  23902  flimclslem  23928  fclsfnflim  23971  flimfnfcls  23972  imasdsf1olem  24317  limcdif  25833  jensenlem1  26953  jensenlem2  26954  jensen  26955  gsumvsca1  33308  gsumvsca2  33309  qsdrngilem  33575  fldgenfldext  33825  evls1fldgencl  33827  fldextrspunlem1  33832  fldextrspunfld  33833  algextdeglem1  33874  algextdeglem2  33875  algextdeglem3  33876  algextdeglem4  33877  constrextdg2lem  33905  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  ordtconnlem1  34081  ssmcls  35761  mclsppslem  35777  rngunsnply  43407  mptrcllem  43850  clcnvlem  43860  brtrclfv2  43964  isotone1  44285  dvnprodlem1  46186