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

Theorem 3ad2antr1 1120
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 697 . 2  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
323adantr3 1116 1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ispod  4338  dfwe2  4589  poxp  6243  cfcoflem  7914  axdc3lem  8092  fzosubel2  10925  sqr0lem  11742  iscatd2  13599  curf2cl  14021  yonedalem4c  14067  grpsubadd  14569  mulgnnass  14611  mulgnn0ass  14612  dprdss  15280  dprd2da  15293  lsssn0  15721  psrbaglesupp  16130  zntoslem  16526  blsscls  18069  iimulcl  18451  pi1grplem  18563  pi1xfrf  18567  dvconst  19282  logexprlim  20480  nvss  21165  disjdsct  23384  issgon  23499  measdivcstOLD  23566  measdivcst  23567  grpodlcan  25479  ismonb2  25915  isepib2  25925  fzadd2  26547  fdc  26558  constr3trllem1  28396  cvrnbtwn3  30088  paddasslem9  30639  paddasslem17  30647  pmapjlln1  30666  lautj  30904  lautm  30905
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator