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

Theorem 3adantr3 1149
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 985 . 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 965
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 967
This theorem is referenced by:  3ad2antr1  1153  3ad2antr2  1154  3adant3r3  1198  sotr2  4665  dfwe2  6388  smogt  6820  wlogle  9865  tanadd  13443  prdsmndd  15446  imasrng  16699  prdslmodd  17027  mpllsslem  17488  mpllsslemOLD  17490  mdetunilem3  18395  ptclsg  19163  tmdgsum2  19642  isxmet2d  19877  xmetres2  19911  prdsxmetlem  19918  comet  20063  iimulcl  20484  icoopnst  20486  iocopnst  20487  icccvx  20497  dvfsumrlim  21478  dvfsumrlim2  21479  eengtrkg  23182  grponpncan  23693  nvsubadd  23986  dmdsl3  25670  rescon  27087  ftc1anclem7  28426  ftc1anc  28428  fzadd2  28590  isdrngo2  28717  iscringd  28752  unichnidl  28784  wwlknredwwlkn  30311  lincresunit3lem2  30903  lincresunit3  30904  lplnle  33024  2llnjN  33051  2lplnj  33104  osumcllem11N  33450  cdleme1  33711  erngplus2  34288  erngplus2-rN  34296  erngdvlem3  34474  erngdvlem3-rN  34482  dvaplusgv  34494  dvalveclem  34510  dvhvaddass  34582  dvhlveclem  34593  dihmeetlem12N  34803
  Copyright terms: Public domain W3C validator