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

Theorem 3ad2antr2 1196
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 730 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1191 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  axdc4lem  8903  ioc0  11708  funcestrcsetclem9  16111  funcsetcestrclem9  16126  grpsubadd  16820  psrbaglesupp  18669  zntoslem  19204  trcfilu  21387  constr2wlk  25407  constr2trl  25408  constr3trllem1  25457  grpopnpcan2  26062  mdsl3  28050  dvrcan5  28630  brofs2  30915  brifs2  30916  poimirlem28  32032  ftc1anc  32089  frinfm  32126  welb  32127  fdc  32138  unichnidl  32328  cvrnbtwn2  32912  islpln2a  33184  paddss1  33453  paddss2  33454  paddasslem17  33472  tendospass  34658  funcringcsetcALTV2lem9  40554  funcringcsetclem9ALTV  40577  ldepsprlem  40773
  Copyright terms: Public domain W3C validator