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

Theorem 3adantr3 1157
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 993 . 2  |-  ( ( ps  /\  ch  /\  ta )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 474 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  3ad2antr1  1161  3ad2antr2  1162  3adant3r3  1207  sotr2  4829  dfwe2  6596  smogt  7038  wlogle  10085  tanadd  13762  prdsmndd  15771  imasrng  17064  prdslmodd  17410  mpllsslem  17881  mpllsslemOLD  17883  scmatlss  18810  mdetunilem3  18899  ptclsg  19867  tmdgsum2  20346  isxmet2d  20581  xmetres2  20615  prdsxmetlem  20622  comet  20767  iimulcl  21188  icoopnst  21190  iocopnst  21191  icccvx  21201  dvfsumrlim  22183  dvfsumrlim2  22184  eengtrkg  23980  wwlknredwwlkn  24418  grponpncan  24949  nvsubadd  25242  dmdsl3  26926  rescon  28347  ftc1anclem7  29689  ftc1anc  29691  fzadd2  29853  isdrngo2  29980  iscringd  30015  unichnidl  30047  lincresunit3lem2  32171  lincresunit3  32172  lplnle  34345  2llnjN  34372  2lplnj  34425  osumcllem11N  34771  cdleme1  35032  erngplus2  35609  erngplus2-rN  35617  erngdvlem3  35795  erngdvlem3-rN  35803  dvaplusgv  35815  dvalveclem  35831  dvhvaddass  35903  dvhlveclem  35914  dihmeetlem12N  36124
  Copyright terms: Public domain W3C validator