Theorem unssad 4147

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  naddcllem  8614  ersym  8658  findcard2d  9103  finsschain  9271  r0weon  9934  ackbij1lem16  10156  wunex2  10661  sumsplit  15703  fsumabs  15736  fsumiun  15756  mrieqvlemd  17564  yonedalem1  18207  yonedalem21  18208  yonedalem22  18213  yonffthlem  18217  lsmsp  21050  mplcoe1  22004  mdetunilem9  22576  ordtbas  23148  isufil2  23864  ufileu  23875  filufint  23876  fmfnfm  23914  flimclslem  23940  fclsfnflim  23983  flimfnfcls  23984  imasdsf1olem  24329  limcdif  25845  jensenlem1  26965  jensenlem2  26966  jensen  26967  gsumvsca1  33319  gsumvsca2  33320  qsdrngilem  33586  fldgenfldext  33845  evls1fldgencl  33847  fldextrspunlem1  33852  fldextrspunfld  33853  algextdeglem1  33894  algextdeglem2  33895  algextdeglem3  33896  algextdeglem4  33897  constrextdg2lem  33925  constrllcllem  33929  constrlccllem  33930  constrcccllem  33931  ordtconnlem1  34101  ssmcls  35780  mclsppslem  35796  rngunsnply  43520  mptrcllem  43963  clcnvlem  43973  brtrclfv2  44077  isotone1  44398  dvnprodlem1  46298