Theorem unssad 3622

Description: If ( A u. B ) is contained in C, so is A. One-way deduction form of unss 3619. Partial converse of unssd 3621. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unssad.1	|- ( ph -> ( A u. B ) C_ C )

Assertion

Ref	Expression
unssad	|- ( ph -> A C_ C )

Proof of Theorem unssad

Step	Hyp	Ref	Expression
1		unssad.1	. . 3 |- ( ph -> ( A u. B ) C_ C )
2		unss 3619	. . 3 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
3	1, 2	sylibr 217	. 2 |- ( ph -> ( A C_ C /\ B C_ C ) )
4	3	simpld 465	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   /\ wa 375   u. cun 3413   C_ wss 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-in 3422  df-ss 3429

This theorem is referenced by:  ersym  7400  findcard2d  7838  finsschain  7906  r0weon  8468  ackbij1lem16  8690  wunex2  9188  sumsplit  13877  fsumabs  13909  fsumiun  13929  mrieqvlemd  15583  yonedalem1  16205  yonedalem21  16206  yonedalem22  16211  yonffthlem  16215  lsmsp  18357  mplcoe1  18737  mdetunilem9  19693  ordtbas  20256  isufil2  20971  ufileu  20982  filufint  20983  fmfnfm  21021  flimclslem  21047  fclsfnflim  21090  flimfnfcls  21091  imasdsf1olem  21436  mbfeqalem  22646  limcdif  22879  jensenlem1  23960  jensenlem2  23961  jensen  23962  gsumvsca1  28593  gsumvsca2  28594  ordtconlem1  28778  ssmcls  30253  mclsppslem  30269  rngunsnply  36083  mptrcllem  36264  clcnvlem  36274  brtrclfv2  36363  dvnprodlem1  37858