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  1197  swopo  4762  omeulem1  7134  divmuldiv  10145  imasmnd2  15580  imasgrp2  15792  srgbinomlem2  16765  imasrng  16837  abvdiv  17048  mdetunilem9  18561  lly1stc  19235  icccvx  20657  dchrpt  22742  vcsubdir  24106  dipsubdir  24420  fdc  28809  unichnidl  28999  dmncan1  29044  pexmidlem6N  33977  erngdvlem3  34992  erngdvlem3-rN  35000  dvalveclem  35028  dvhvaddass  35100  dvhlveclem  35111
  Copyright terms: Public domain W3C validator