Theorem unssbd 4144

Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4140. Partial converse of unssd 4142. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unssad.1	⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)

Assertion

Ref	Expression
unssbd	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem unssbd

Step	Hyp	Ref	Expression
1		unssad.1	. . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
2		unss 4140	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 234	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simprd 495	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3900   ⊆ wss 3902

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919

This theorem is referenced by:  eldifpw  7701  naddcllem  8591  ertr  8637  finsschain  9243  r0weon  9903  ackbij1lem16  10125  wunfi  10612  wunex2  10629  hashf1lem2  14363  sumsplit  15675  fsum2dlem  15677  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  fprod2dlem  15887  mreexexlem3d  17552  yonedalem1  18178  yonedalem21  18179  yonedalem3a  18180  yonedalem4c  18183  yonedalem22  18184  yonedalem3b  18185  yonedainv  18187  yonffthlem  18188  ablfac1eulem  19987  lsmsp  21021  lsppratlem3  21087  mplcoe1  21973  mdetunilem9  22536  filufint  23836  fmfnfmlem4  23873  hausflim  23897  fclsfnflim  23943  fsumcn  24789  itgfsum  25756  jensenlem1  26925  jensenlem2  26926  gsumvsca1  33193  gsumvsca2  33194  qsdrngilem  33457  evls1fldgencl  33681  fldextrspunlem1  33686  constrextdg2lem  33759  constrllcllem  33763  constrlccllem  33764  constrcccllem  33765  ordtconnlem1  33935  vhmcls  35608  mclsppslem  35625  rngunsnply  43208  brtrclfv2  43766