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

Theorem 3ad2antr2 1154
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antr2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )

Proof of Theorem 3ad2antr2
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantrl 715 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1149 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  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:  axdc4lem  8645  ioc0  11368  grpsubadd  15634  psrbaglesupp  17457  zntoslem  18011  trcfilu  19891  constr2wlk  23519  constr2trl  23520  constr3trllem1  23558  grpopnpcan2  23762  mdsl3  25742  dvrcan5  26283  brofs2  28130  brifs2  28131  ftc1anc  28501  frinfm  28655  welb  28656  fdc  28667  unichnidl  28857  ldepsprlem  31003  cvrnbtwn2  33016  islpln2a  33288  paddss1  33557  paddss2  33558  paddasslem17  33576  tendospass  34760
  Copyright terms: Public domain W3C validator