Theorem unssad 4159

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
unssad	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem unssad

Step	Hyp	Ref	Expression
1		unssad.1	. . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)
2		unss 4156	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
3	1, 2	sylibr 234	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
4	3	simpld 494	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:  naddcllem  8643  ersym  8686  findcard2d  9136  finsschain  9317  r0weon  9972  ackbij1lem16  10194  wunex2  10698  sumsplit  15741  fsumabs  15774  fsumiun  15794  mrieqvlemd  17597  yonedalem1  18240  yonedalem21  18241  yonedalem22  18246  yonffthlem  18250  lsmsp  21000  mplcoe1  21951  mdetunilem9  22514  ordtbas  23086  isufil2  23802  ufileu  23813  filufint  23814  fmfnfm  23852  flimclslem  23878  fclsfnflim  23921  flimfnfcls  23922  imasdsf1olem  24268  limcdif  25784  jensenlem1  26904  jensenlem2  26905  jensen  26906  gsumvsca1  33186  gsumvsca2  33187  qsdrngilem  33472  fldgenfldext  33670  evls1fldgencl  33672  fldextrspunlem1  33677  fldextrspunfld  33678  algextdeglem1  33714  algextdeglem2  33715  algextdeglem3  33716  algextdeglem4  33717  constrextdg2lem  33745  constrllcllem  33749  constrlccllem  33750  constrcccllem  33751  ordtconnlem1  33921  ssmcls  35561  mclsppslem  35577  rngunsnply  43165  mptrcllem  43609  clcnvlem  43619  brtrclfv2  43723  isotone1  44044  dvnprodlem1  45951