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

Theorem 3ad2antr1 1153
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 1149 1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ispod  4664  dfwe2  6408  poxp  6699  cfcoflem  8456  axdc3lem  8634  fzosubel2  11615  sqr0lem  12745  iscatd2  14634  curf2cl  15056  yonedalem4c  15102  grpsubadd  15628  mulgnnass  15670  mulgnn0ass  15671  dprdss  16541  dprd2da  16556  lsssn0  17044  psrbaglesupp  17450  psrbaglesuppOLD  17451  zntoslem  18004  blsscls  20097  iimulcl  20524  pi1grplem  20636  pi1xfrf  20640  dvconst  21406  logexprlim  22579  constr3trllem1  23551  nvss  23986  disjdsct  26013  issgon  26581  measdivcstOLD  26653  measdivcst  26654  ftc1anc  28494  fzadd2  28656  fdc  28660  wwlknextbi  30376  lincresunit3lem2  31033  cvrnbtwn3  32940  paddasslem9  33491  paddasslem17  33499  pmapjlln1  33518  lautj  33756  lautm  33757
  Copyright terms: Public domain W3C validator