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  4340  omeulem1  6596  divmuldiv  9476  imasmnd2  14425  imasgrp2  14626  imasrng  15418  abvdiv  15618  lly1stc  17238  icccvx  18464  dchrpt  20522  vcsubdir  21128  dipsubdir  21442  dblsubvec  25577  mvecrtol2  25580  fdc  26558  unichnidl  26759  dmncan1  26804  pexmidlem6N  30786  erngdvlem3  31801  erngdvlem3-rN  31809  dvalveclem  31837  dvhvaddass  31909  dvhlveclem  31920
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