Theorem unssad 4203

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3961   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980

This theorem is referenced by:  naddcllem  8713  ersym  8756  findcard2d  9205  finsschain  9397  r0weon  10050  ackbij1lem16  10272  wunex2  10776  sumsplit  15801  fsumabs  15834  fsumiun  15854  mrieqvlemd  17674  yonedalem1  18329  yonedalem21  18330  yonedalem22  18335  yonffthlem  18339  lsmsp  21103  mplcoe1  22073  mdetunilem9  22642  ordtbas  23216  isufil2  23932  ufileu  23943  filufint  23944  fmfnfm  23982  flimclslem  24008  fclsfnflim  24051  flimfnfcls  24052  imasdsf1olem  24399  limcdif  25926  jensenlem1  27045  jensenlem2  27046  jensen  27047  gsumvsca1  33215  gsumvsca2  33216  qsdrngilem  33502  fldgenfldext  33693  evls1fldgencl  33695  algextdeglem1  33723  algextdeglem2  33724  algextdeglem3  33725  algextdeglem4  33726  ordtconnlem1  33885  ssmcls  35552  mclsppslem  35568  rngunsnply  43158  mptrcllem  43603  clcnvlem  43613  brtrclfv2  43717  isotone1  44038  dvnprodlem1  45902