Theorem unssad 3620

Description: If ( A u. B ) is contained in C, so is A. One-way deduction form of unss 3617. Partial converse of unssd 3619. (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 3617	. . 3 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
3	1, 2	sylibr 212	. 2 |- ( ph -> ( A C_ C /\ B C_ C ) )
4	3	simpld 457	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   /\ wa 367   u. cun 3412   C_ wss 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-un 3419  df-in 3421  df-ss 3428

This theorem is referenced by:  ersym  7360  findcard2d  7796  finsschain  7861  r0weon  8422  ackbij1lem16  8647  wunex2  9146  sumsplit  13734  fsumabs  13766  fsumiun  13786  mrieqvlemd  15243  yonedalem1  15865  yonedalem21  15866  yonedalem22  15871  yonffthlem  15875  lsmsp  18052  mplcoe1  18447  mdetunilem9  19414  ordtbas  19986  isufil2  20701  ufileu  20712  filufint  20713  fmfnfm  20751  flimclslem  20777  fclsfnflim  20820  flimfnfcls  20821  imasdsf1olem  21168  mbfeqalem  22341  limcdif  22572  jensenlem1  23642  jensenlem2  23643  jensen  23644  gsumvsca1  28225  gsumvsca2  28226  ordtconlem1  28359  ssmcls  29779  mclsppslem  29795  rngunsnply  35486  brtrclfv2  35706  dvnprodlem1  37111