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

Theorem 3ad2antr1 1162
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 716 . 2  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
323adantr3 1158 1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976
This theorem is referenced by:  ispod  4798  dfwe2  6602  poxp  6897  cfcoflem  8655  axdc3lem  8833  fzosubel2  11858  sqr0lem  13056  iscatd2  15060  curf2cl  15479  yonedalem4c  15525  grpsubadd  16105  mulgnnass  16149  mulgnn0ass  16150  dprdss  17055  dprd2da  17070  srgi  17142  lsssn0  17573  psrbaglesupp  17996  psrbaglesuppOLD  17997  zntoslem  18573  blsscls  20988  iimulcl  21415  pi1grplem  21527  pi1xfrf  21531  dvconst  22298  logexprlim  23478  constr3trllem1  24628  wwlknextbi  24703  nvss  25464  disjdsct  27499  issgon  28101  measdivcstOLD  28173  measdivcst  28174  elmrsubrn  28858  ftc1anc  30074  fzadd2  30210  fdc  30214  lidldomnnring  32563  funcestrcsetclem9  32620  funcsetcestrclem9  32635  funcringcsetcOLD2lem9  32724  funcringcsetclem9OLD  32747  lincresunit3lem2  32951  cvrnbtwn3  34876  paddasslem9  35427  paddasslem17  35435  pmapjlln1  35454  lautj  35692  lautm  35693
  Copyright terms: Public domain W3C validator