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

Theorem 3ad2antr1 1122
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antr1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )

Proof of Theorem 3ad2antr1
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantrr 698 . 2  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
323adantr3 1118 1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ispod  4511  dfwe2  4762  poxp  6458  cfcoflem  8152  axdc3lem  8330  fzosubel2  11178  sqr0lem  12046  iscatd2  13906  curf2cl  14328  yonedalem4c  14374  grpsubadd  14876  mulgnnass  14918  mulgnn0ass  14919  dprdss  15587  dprd2da  15600  lsssn0  16024  psrbaglesupp  16433  zntoslem  16837  blsscls  18537  iimulcl  18962  pi1grplem  19074  pi1xfrf  19078  dvconst  19803  logexprlim  21009  constr3trllem1  21637  nvss  22072  disjdsct  24090  issgon  24506  measdivcstOLD  24578  measdivcst  24579  ftc1anc  26288  fzadd2  26445  fdc  26449  swrdccatin2lem1  28206  2cshw1lem1  28248  2cshw1lem2  28249  2cshw1  28251  2cshw2lem2  28253  2cshw2  28255  cvrnbtwn3  30074  paddasslem9  30625  paddasslem17  30633  pmapjlln1  30652  lautj  30890  lautm  30891
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator