Theorem unssad 4156

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3912   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  naddcllem  8640  ersym  8683  findcard2d  9130  finsschain  9310  r0weon  9965  ackbij1lem16  10187  wunex2  10691  sumsplit  15734  fsumabs  15767  fsumiun  15787  mrieqvlemd  17590  yonedalem1  18233  yonedalem21  18234  yonedalem22  18239  yonffthlem  18243  lsmsp  20993  mplcoe1  21944  mdetunilem9  22507  ordtbas  23079  isufil2  23795  ufileu  23806  filufint  23807  fmfnfm  23845  flimclslem  23871  fclsfnflim  23914  flimfnfcls  23915  imasdsf1olem  24261  limcdif  25777  jensenlem1  26897  jensenlem2  26898  jensen  26899  gsumvsca1  33179  gsumvsca2  33180  qsdrngilem  33465  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlem1  33670  fldextrspunfld  33671  algextdeglem1  33707  algextdeglem2  33708  algextdeglem3  33709  algextdeglem4  33710  constrextdg2lem  33738  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  ordtconnlem1  33914  ssmcls  35554  mclsppslem  35570  rngunsnply  43158  mptrcllem  43602  clcnvlem  43612  brtrclfv2  43716  isotone1  44037  dvnprodlem1  45944