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

Theorem 3ad2antr1 1161
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 1157 1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  ispod  4808  dfwe2  6595  poxp  6892  cfcoflem  8648  axdc3lem  8826  fzosubel2  11840  sqr0lem  13033  iscatd2  14932  curf2cl  15354  yonedalem4c  15400  grpsubadd  15927  mulgnnass  15970  mulgnn0ass  15971  dprdss  16866  dprd2da  16881  lsssn0  17377  psrbaglesupp  17788  psrbaglesuppOLD  17789  zntoslem  18362  blsscls  20745  iimulcl  21172  pi1grplem  21284  pi1xfrf  21288  dvconst  22055  logexprlim  23228  legso  23712  constr3trllem1  24326  wwlknextbi  24401  nvss  25162  disjdsct  27193  issgon  27763  measdivcstOLD  27835  measdivcst  27836  ftc1anc  29675  fzadd2  29837  fdc  29841  lincresunit3lem2  32154  cvrnbtwn3  34073  paddasslem9  34624  paddasslem17  34632  pmapjlln1  34651  lautj  34889  lautm  34890
  Copyright terms: Public domain W3C validator