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

Theorem 3adantr1 1114
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 954 . 2  |-  ( ( ta  /\  ps  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ad2antr3  1122  3adant3r1  1160  swopo  4324  omeulem1  6580  divmuldiv  9460  imasmnd2  14409  imasgrp2  14610  imasrng  15402  abvdiv  15602  lly1stc  17222  icccvx  18448  dchrpt  20506  vcsubdir  21112  dipsubdir  21426  dblsubvec  25474  mvecrtol2  25477  fdc  26455  unichnidl  26656  dmncan1  26701  pexmidlem6N  30164  erngdvlem3  31179  erngdvlem3-rN  31187  dvalveclem  31215  dvhvaddass  31287  dvhlveclem  31298
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator