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

Theorem 3adantr3 1116
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 952 . 2  |-  ( ( ps  /\  ch  /\  ta )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ad2antr1  1120  3ad2antr2  1121  3adant3r3  1162  sotr2  4343  dfwe2  4573  smogt  6384  wlogle  9306  tanadd  12447  prdsmndd  14405  imasrng  15402  prdslmodd  15726  mpllsslem  16180  ptclsg  17309  tmdgsum2  17779  isxmet2d  17892  xmetres2  17925  prdsxmetlem  17932  comet  18059  iimulcl  18435  icoopnst  18437  iocopnst  18438  icccvx  18448  dvfsumrlim  19378  dvfsumrlim2  19379  grponpncan  20922  nvsubadd  21213  dmdsl3  22895  rescon  23777  dblsubvec  25474  fzadd2  26444  isdrngo2  26589  iscringd  26624  unichnidl  26656  lplnle  29729  2llnjN  29756  2lplnj  29809  osumcllem11N  30155  cdleme1  30416  erngplus2  30993  erngplus2-rN  31001  erngdvlem3  31179  erngdvlem3-rN  31187  dvaplusgv  31199  dvalveclem  31215  dvhvaddass  31287  dvhlveclem  31298  dihmeetlem12N  31508
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