Theorem unssad 4158

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3921  df-ss 3933

This theorem is referenced by:  naddcllem  8642  ersym  8685  findcard2d  9135  finsschain  9316  r0weon  9971  ackbij1lem16  10193  wunex2  10697  sumsplit  15740  fsumabs  15773  fsumiun  15793  mrieqvlemd  17596  yonedalem1  18239  yonedalem21  18240  yonedalem22  18245  yonffthlem  18249  lsmsp  20999  mplcoe1  21950  mdetunilem9  22513  ordtbas  23085  isufil2  23801  ufileu  23812  filufint  23813  fmfnfm  23851  flimclslem  23877  fclsfnflim  23920  flimfnfcls  23921  imasdsf1olem  24267  limcdif  25783  jensenlem1  26903  jensenlem2  26904  jensen  26905  gsumvsca1  33185  gsumvsca2  33186  qsdrngilem  33471  fldgenfldext  33669  evls1fldgencl  33671  fldextrspunlem1  33676  fldextrspunfld  33677  algextdeglem1  33713  algextdeglem2  33714  algextdeglem3  33715  algextdeglem4  33716  constrextdg2lem  33744  constrllcllem  33748  constrlccllem  33749  constrcccllem  33750  ordtconnlem1  33920  ssmcls  35554  mclsppslem  35570  rngunsnply  43151  mptrcllem  43595  clcnvlem  43605  brtrclfv2  43709  isotone1  44030  dvnprodlem1  45937