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 236	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simpld 498	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921

This theorem is referenced by:  naddcllem  8641  ersym  8686  findcard2d  9131  finsschain  9299  r0weon  9965  ackbij1lem16  10187  wunex2  10693  sumsplit  15778  fsumabs  15812  fsumiun  15832  mrieqvlemd  17644  yonedalem1  18287  yonedalem21  18288  yonedalem22  18293  yonffthlem  18297  lsmsp  21133  mplcoe1  22070  mdetunilem9  22660  ordtbas  23232  isufil2  23948  ufileu  23959  filufint  23960  fmfnfm  23998  flimclslem  24024  fclsfnflim  24067  flimfnfcls  24068  imasdsf1olem  24413  limcdif  25918  jensenlem1  27028  jensenlem2  27029  jensen  27030  gsumvsca1  33367  gsumvsca2  33368  qsdrngilem  33643  fldgenfldext  33926  evls1fldgencl  33928  fldextrspunlem1  33933  fldextrspunfld  33934  algextdeglem1  33975  algextdeglem2  33976  algextdeglem3  33977  algextdeglem4  33978  constrextdg2lem  34006  constrllcllem  34010  constrlccllem  34011  constrcccllem  34012  ordtconnlem1  34182  ssmcls  35881  mclsppslem  35897  rngunsnply  43710  mptrcllem  44153  clcnvlem  44163  brtrclfv2  44267  isotone1  44588  dvnprodlem1  46484