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  1199  sotr2  4781  dfwe2  6506  smogt  6941  wlogle  9987  tanadd  13572  prdsmndd  15576  imasrng  16837  prdslmodd  17176  mpllsslem  17638  mpllsslemOLD  17640  mdetunilem3  18555  ptclsg  19323  tmdgsum2  19802  isxmet2d  20037  xmetres2  20071  prdsxmetlem  20078  comet  20223  iimulcl  20644  icoopnst  20646  iocopnst  20647  icccvx  20657  dvfsumrlim  21639  dvfsumrlim2  21640  eengtrkg  23403  grponpncan  23914  nvsubadd  24207  dmdsl3  25891  rescon  27299  ftc1anclem7  28641  ftc1anc  28643  fzadd2  28805  isdrngo2  28932  iscringd  28967  unichnidl  28999  wwlknredwwlkn  30526  lincresunit3lem2  31166  lincresunit3  31167  lplnle  33542  2llnjN  33569  2lplnj  33622  osumcllem11N  33968  cdleme1  34229  erngplus2  34806  erngplus2-rN  34814  erngdvlem3  34992  erngdvlem3-rN  35000  dvaplusgv  35012  dvalveclem  35028  dvhvaddass  35100  dvhlveclem  35111  dihmeetlem12N  35321
  Copyright terms: Public domain W3C validator