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

Theorem 3adantr1 1156
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 996 . 2  |-  ( ( ta  /\  ps  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 472 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  3ad2antr3  1164  3adant3r1  1206  swopo  4753  omeulem1  7267  divmuldiv  10284  imasmnd2  16279  imasgrp2  16507  srgbinomlem2  17510  imasring  17586  abvdiv  17804  mdetunilem9  19412  lly1stc  20287  icccvx  21740  dchrpt  23921  vcsubdir  25849  dipsubdir  26163  fdc  31500  unichnidl  31690  dmncan1  31735  pexmidlem6N  32972  erngdvlem3  33989  erngdvlem3-rN  33997  dvalveclem  34025  dvhvaddass  34097  dvhlveclem  34108
  Copyright terms: Public domain W3C validator