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

Theorem 3ad2antr1 1148
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 711 . 2  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
323adantr3 1144 1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  ispod  4645  dfwe2  6392  poxp  6683  cfcoflem  8437  axdc3lem  8615  fzosubel2  11596  sqr0lem  12726  iscatd2  14615  curf2cl  15037  yonedalem4c  15083  grpsubadd  15606  mulgnnass  15648  mulgnn0ass  15649  dprdss  16516  dprd2da  16531  lsssn0  17007  psrbaglesupp  17413  psrbaglesuppOLD  17414  zntoslem  17948  blsscls  20041  iimulcl  20468  pi1grplem  20580  pi1xfrf  20584  dvconst  21350  logexprlim  22523  constr3trllem1  23471  nvss  23906  disjdsct  25933  issgon  26502  measdivcstOLD  26574  measdivcst  26575  ftc1anc  28400  fzadd2  28562  fdc  28566  wwlknextbi  30282  lincresunit3lem2  30855  cvrnbtwn3  32643  paddasslem9  33194  paddasslem17  33202  pmapjlln1  33221  lautj  33459  lautm  33460
  Copyright terms: Public domain W3C validator