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

Theorem 3ad2antr2 1147
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 708 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1142 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  axdc4lem  8612  ioc0  11334  grpsubadd  15592  psrbaglesupp  17368  zntoslem  17830  trcfilu  19710  constr2wlk  23319  constr2trl  23320  constr3trllem1  23358  grpopnpcan2  23562  mdsl3  25542  dvrcan5  26113  brofs2  27954  brifs2  27955  ftc1anc  28316  frinfm  28470  welb  28471  fdc  28482  unichnidl  28672  ldepsprlem  30712  cvrnbtwn2  32490  islpln2a  32762  paddss1  33031  paddss2  33032  paddasslem17  33050  tendospass  34234
  Copyright terms: Public domain W3C validator