Theorem unssad 4216

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  naddcllem  8732  ersym  8775  findcard2d  9232  finsschain  9429  r0weon  10081  ackbij1lem16  10303  wunex2  10807  sumsplit  15816  fsumabs  15849  fsumiun  15869  mrieqvlemd  17687  yonedalem1  18342  yonedalem21  18343  yonedalem22  18348  yonffthlem  18352  lsmsp  21108  mplcoe1  22078  mdetunilem9  22647  ordtbas  23221  isufil2  23937  ufileu  23948  filufint  23949  fmfnfm  23987  flimclslem  24013  fclsfnflim  24056  flimfnfcls  24057  imasdsf1olem  24404  limcdif  25931  jensenlem1  27048  jensenlem2  27049  jensen  27050  gsumvsca1  33205  gsumvsca2  33206  qsdrngilem  33487  fldgenfldext  33678  evls1fldgencl  33680  algextdeglem1  33708  algextdeglem2  33709  algextdeglem3  33710  algextdeglem4  33711  ordtconnlem1  33870  ssmcls  35535  mclsppslem  35551  rngunsnply  43130  mptrcllem  43575  clcnvlem  43585  brtrclfv2  43689  isotone1  44010  dvnprodlem1  45867