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

Theorem 3adantr2 1115
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
3adantr2  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )

Proof of Theorem 3adantr2
StepHypRef Expression
1 3simpb 953 . 2  |-  ( ( ps  /\  ta  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3adant3r2  1161  po3nr  4328  sornom  7903  axdclem2  8147  fzm1  10862  issubc3  13723  joinle  14127  pgpfi  14916  imasrng  15402  prdslmodd  15726  icoopnst  18437  iocopnst  18438  nvmdi  21208  mdsl3  22896  axcontlem4  24595  elicc3  26228  fzadd2  26444  iscringd  26624  erngdvlem3  31179  erngdvlem3-rN  31187  dvalveclem  31215  dvhlveclem  31298
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