Theorem unssad 3526

Description: If ( A u. B ) is contained in C, so is A. One-way deduction form of unss 3523. Partial converse of unssd 3525. (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 3523	. . 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 459	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   /\ wa 369   u. cun 3319   C_ wss 3321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2968  df-un 3326  df-in 3328  df-ss 3335

This theorem is referenced by:  ersym  7105  findcard2d  7546  finsschain  7610  r0weon  8171  ackbij1lem16  8396  wunex2  8897  sumsplit  13227  fsumabs  13256  fsumiun  13276  mrieqvlemd  14559  yonedalem1  15074  yonedalem21  15075  yonedalem22  15080  yonffthlem  15084  lsmsp  17141  mplcoe1  17518  mdetunilem9  18395  ordtbas  18765  isufil2  19450  ufileu  19461  filufint  19462  fmfnfm  19500  flimclslem  19526  fclsfnflim  19569  flimfnfcls  19570  imasdsf1olem  19917  mbfeqalem  21089  limcdif  21320  jensenlem1  22349  jensenlem2  22350  jensen  22351  ordtconlem1  26302  rngunsnply  29473