Theorem unssad 4146

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

Syntax hints:   → wi 4   ∧ wa 398   ∪ cun 3917   ⊆ wss 3919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-v 3483  df-un 3924  df-in 3926  df-ss 3935

This theorem is referenced by:  ersym  8282  findcard2d  8741  finsschain  8812  r0weon  9419  ackbij1lem16  9638  wunex2  10141  sumsplit  15103  fsumabs  15136  fsumiun  15156  mrieqvlemd  16878  yonedalem1  17500  yonedalem21  17501  yonedalem22  17506  yonffthlem  17510  lsmsp  19836  mplcoe1  20224  mdetunilem9  21207  ordtbas  21778  isufil2  22494  ufileu  22505  filufint  22506  fmfnfm  22544  flimclslem  22570  fclsfnflim  22613  flimfnfcls  22614  imasdsf1olem  22961  limcdif  24454  jensenlem1  25545  jensenlem2  25546  jensen  25547  gsumvsca1  30856  gsumvsca2  30857  ordtconnlem1  31169  ssmcls  32816  mclsppslem  32832  rngunsnply  39860  mptrcllem  40058  clcnvlem  40068  brtrclfv2  40157  isotone1  40483  dvnprodlem1  42316