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

Theorem 3adantr3 1119
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
3adantr3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )

Proof of Theorem 3adantr3
StepHypRef Expression
1 3simpa 955 . 2  |-  ( ( ps  /\  ch  /\  ta )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 462 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3ad2antr1  1123  3ad2antr2  1124  3adant3r3  1165  sotr2  4533  dfwe2  4763  smogt  6630  wlogle  9561  tanadd  12769  prdsmndd  14729  imasrng  15726  prdslmodd  16046  mpllsslem  16500  ptclsg  17648  tmdgsum2  18127  isxmet2d  18358  xmetres2  18392  prdsxmetlem  18399  comet  18544  iimulcl  18963  icoopnst  18965  iocopnst  18966  icccvx  18976  dvfsumrlim  19916  dvfsumrlim2  19917  grponpncan  21844  nvsubadd  22137  dmdsl3  23819  rescon  24934  ftc1anclem7  26287  ftc1anc  26289  fzadd2  26446  isdrngo2  26575  iscringd  26610  unichnidl  26642  lplnle  30338  2llnjN  30365  2lplnj  30418  osumcllem11N  30764  cdleme1  31025  erngplus2  31602  erngplus2-rN  31610  erngdvlem3  31788  erngdvlem3-rN  31796  dvaplusgv  31808  dvalveclem  31824  dvhvaddass  31896  dvhlveclem  31907  dihmeetlem12N  32117
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator