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

Theorem 3adantr1 1165
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 1005 . 2  |-  ( ( ta  /\  ps  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 477 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  3ad2antr3  1173  3adant3r1  1215  swopo  4782  omeulem1  7289  divmuldiv  10309  imasmnd2  16566  imasgrp2  16794  srgbinomlem2  17767  imasring  17840  abvdiv  18058  mdetunilem9  19637  lly1stc  20503  icccvx  21970  dchrpt  24187  vcsubdir  26167  dipsubdir  26481  poimirlem4  31902  fdc  32032  unichnidl  32222  dmncan1  32267  pexmidlem6N  33503  erngdvlem3  34520  erngdvlem3-rN  34528  dvalveclem  34556  dvhvaddass  34628  dvhlveclem  34639
  Copyright terms: Public domain W3C validator