Theorem unssad 4146

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3903   ⊆ wss 3905

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922

This theorem is referenced by:  naddcllem  8601  ersym  8644  findcard2d  9090  finsschain  9268  r0weon  9925  ackbij1lem16  10147  wunex2  10651  sumsplit  15693  fsumabs  15726  fsumiun  15746  mrieqvlemd  17553  yonedalem1  18196  yonedalem21  18197  yonedalem22  18202  yonffthlem  18206  lsmsp  21008  mplcoe1  21960  mdetunilem9  22523  ordtbas  23095  isufil2  23811  ufileu  23822  filufint  23823  fmfnfm  23861  flimclslem  23887  fclsfnflim  23930  flimfnfcls  23931  imasdsf1olem  24277  limcdif  25793  jensenlem1  26913  jensenlem2  26914  jensen  26915  gsumvsca1  33178  gsumvsca2  33179  qsdrngilem  33441  fldgenfldext  33639  evls1fldgencl  33641  fldextrspunlem1  33646  fldextrspunfld  33647  algextdeglem1  33683  algextdeglem2  33684  algextdeglem3  33685  algextdeglem4  33686  constrextdg2lem  33714  constrllcllem  33718  constrlccllem  33719  constrcccllem  33720  ordtconnlem1  33890  ssmcls  35539  mclsppslem  35555  rngunsnply  43142  mptrcllem  43586  clcnvlem  43596  brtrclfv2  43700  isotone1  44021  dvnprodlem1  45928