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

Theorem 3adantr1 1147
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
3adantr.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
3adantr1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )

Proof of Theorem 3adantr1
StepHypRef Expression
1 3simpc 987 . 2  |-  ( ( ta  /\  ps  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 474 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  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:  3ad2antr3  1155  3adant3r1  1196  swopo  4646  omeulem1  7013  divmuldiv  10023  imasmnd2  15450  imasgrp2  15661  srgbinomlem2  16627  imasrng  16699  abvdiv  16900  mdetunilem9  18401  lly1stc  19075  icccvx  20497  dchrpt  22581  vcsubdir  23885  dipsubdir  24199  fdc  28594  unichnidl  28784  dmncan1  28829  pexmidlem6N  33459  erngdvlem3  34474  erngdvlem3-rN  34482  dvalveclem  34510  dvhvaddass  34582  dvhlveclem  34593
  Copyright terms: Public domain W3C validator