Theorem unssad 4012

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

Syntax hints:   → wi 4   ∧ wa 386   ∪ cun 3789   ⊆ wss 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399  df-un 3796  df-in 3798  df-ss 3805

This theorem is referenced by:  ersym  8038  findcard2d  8490  finsschain  8561  r0weon  9168  ackbij1lem16  9392  wunex2  9895  sumsplit  14904  fsumabs  14937  fsumiun  14957  mrieqvlemd  16675  yonedalem1  17298  yonedalem21  17299  yonedalem22  17304  yonffthlem  17308  lsmsp  19481  mplcoe1  19862  mdetunilem9  20831  ordtbas  21404  isufil2  22120  ufileu  22131  filufint  22132  fmfnfm  22170  flimclslem  22196  fclsfnflim  22239  flimfnfcls  22240  imasdsf1olem  22586  limcdif  24077  jensenlem1  25165  jensenlem2  25166  jensen  25167  gsumvsca1  30344  gsumvsca2  30345  ordtconnlem1  30568  ssmcls  32063  mclsppslem  32079  rngunsnply  38684  mptrcllem  38859  clcnvlem  38869  brtrclfv2  38958  isotone1  39284  dvnprodlem1  41071