Theorem unssad 3644

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

Syntax hints:   -> wi 4   /\ wa 371   u. cun 3435   C_ wss 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442  df-in 3444  df-ss 3451

This theorem is referenced by:  ersym  7381  findcard2d  7817  finsschain  7885  r0weon  8446  ackbij1lem16  8667  wunex2  9165  sumsplit  13822  fsumabs  13854  fsumiun  13874  mrieqvlemd  15528  yonedalem1  16150  yonedalem21  16151  yonedalem22  16156  yonffthlem  16160  lsmsp  18302  mplcoe1  18682  mdetunilem9  19637  ordtbas  20200  isufil2  20915  ufileu  20926  filufint  20927  fmfnfm  20965  flimclslem  20991  fclsfnflim  21034  flimfnfcls  21035  imasdsf1olem  21380  mbfeqalem  22590  limcdif  22823  jensenlem1  23904  jensenlem2  23905  jensen  23906  gsumvsca1  28547  gsumvsca2  28548  ordtconlem1  28732  ssmcls  30207  mclsppslem  30223  rngunsnply  36003  brtrclfv2  36223  dvnprodlem1  37685