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

Theorem 3adantr3 1166
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 1002 . 2  |-  ( ( ps  /\  ch  /\  ta )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 476 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  3ad2antr1  1170  3ad2antr2  1171  3adant3r3  1216  sotr2  4804  dfwe2  6622  smogt  7094  wlogle  10146  tanadd  14199  prdsmndd  16520  mhmmnd  16759  imasring  17782  prdslmodd  18127  mpllsslem  18594  scmatlss  19481  mdetunilem3  19570  ptclsg  20561  tmdgsum2  21042  isxmet2d  21273  xmetres2  21307  prdsxmetlem  21314  comet  21459  iimulcl  21861  icoopnst  21863  iocopnst  21864  icccvx  21874  dvfsumrlim  22860  dvfsumrlim2  22861  colhp  24668  eengtrkg  24861  wwlknredwwlkn  25299  grponpncan  25828  nvsubadd  26121  dmdsl3  27803  rescon  29757  poimirlem28  31671  poimirlem32  31675  broucube  31677  ftc1anclem7  31726  ftc1anc  31728  fzadd2  31773  isdrngo2  31900  iscringd  31935  unichnidl  31967  lplnle  32813  2llnjN  32840  2lplnj  32893  osumcllem11N  33239  cdleme1  33501  erngplus2  34079  erngplus2-rN  34087  erngdvlem3  34265  erngdvlem3-rN  34273  dvaplusgv  34285  dvalveclem  34301  dvhvaddass  34373  dvhlveclem  34384  dihmeetlem12N  34594  lincresunit3lem2  39032  lincresunit3  39033
  Copyright terms: Public domain W3C validator