MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unssad Structured version   Unicode version

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
StepHypRef 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
)
31, 2sylibr 212 . 2  |-  ( ph  ->  ( A  C_  C  /\  B  C_  C ) )
43simpld 459 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator