Theorem unssad 4114

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

Syntax hints:   → wi 4   ∧ wa 399   ∪ cun 3879   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  ersym  8284  findcard2d  8744  finsschain  8815  r0weon  9423  ackbij1lem16  9646  wunex2  10149  sumsplit  15115  fsumabs  15148  fsumiun  15168  mrieqvlemd  16892  yonedalem1  17514  yonedalem21  17515  yonedalem22  17520  yonffthlem  17524  lsmsp  19851  mplcoe1  20705  mdetunilem9  21225  ordtbas  21797  isufil2  22513  ufileu  22524  filufint  22525  fmfnfm  22563  flimclslem  22589  fclsfnflim  22632  flimfnfcls  22633  imasdsf1olem  22980  limcdif  24479  jensenlem1  25572  jensenlem2  25573  jensen  25574  gsumvsca1  30904  gsumvsca2  30905  ordtconnlem1  31277  ssmcls  32927  mclsppslem  32943  rngunsnply  40117  mptrcllem  40313  clcnvlem  40323  brtrclfv2  40428  isotone1  40751  dvnprodlem1  42588