Theorem unssbd 4160

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3915   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934

This theorem is referenced by:  eldifpw  7747  naddcllem  8643  ertr  8689  finsschain  9317  r0weon  9972  ackbij1lem16  10194  wunfi  10681  wunex2  10698  hashf1lem2  14428  sumsplit  15741  fsum2dlem  15743  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  fprod2dlem  15953  mreexexlem3d  17614  yonedalem1  18240  yonedalem21  18241  yonedalem3a  18242  yonedalem4c  18245  yonedalem22  18246  yonedalem3b  18247  yonedainv  18249  yonffthlem  18250  ablfac1eulem  20011  lsmsp  21000  lsppratlem3  21066  mplcoe1  21951  mdetunilem9  22514  filufint  23814  fmfnfmlem4  23851  hausflim  23875  fclsfnflim  23921  fsumcn  24768  itgfsum  25735  jensenlem1  26904  jensenlem2  26905  gsumvsca1  33186  gsumvsca2  33187  qsdrngilem  33472  evls1fldgencl  33672  fldextrspunlem1  33677  constrextdg2lem  33745  constrllcllem  33749  constrlccllem  33750  constrcccllem  33751  ordtconnlem1  33921  vhmcls  35560  mclsppslem  35577  rngunsnply  43165  brtrclfv2  43723