Theorem unssad 4188

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

Syntax hints:   → wi 4   ∧ wa 394   ∪ cun 3945   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-ss 3964

This theorem is referenced by:  naddcllem  8706  ersym  8746  findcard2d  9204  finsschain  9403  r0weon  10055  ackbij1lem16  10278  wunex2  10781  sumsplit  15772  fsumabs  15805  fsumiun  15825  mrieqvlemd  17642  yonedalem1  18297  yonedalem21  18298  yonedalem22  18303  yonffthlem  18307  lsmsp  21064  mplcoe1  22044  mdetunilem9  22613  ordtbas  23187  isufil2  23903  ufileu  23914  filufint  23915  fmfnfm  23953  flimclslem  23979  fclsfnflim  24022  flimfnfcls  24023  imasdsf1olem  24370  limcdif  25896  jensenlem1  27015  jensenlem2  27016  jensen  27017  gsumvsca1  33090  gsumvsca2  33091  qsdrngilem  33369  fldgenfldext  33554  evls1fldgencl  33556  algextdeglem1  33584  algextdeglem2  33585  algextdeglem3  33586  algextdeglem4  33587  ordtconnlem1  33739  ssmcls  35395  mclsppslem  35411  rngunsnply  42834  mptrcllem  43280  clcnvlem  43290  brtrclfv2  43394  isotone1  43715  dvnprodlem1  45567