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

Theorem 3adantr2 1151
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 989 . 2  |-  ( ( ps  /\  ta  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 474 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  3adant3r2  1201  po3nr  4807  sornom  8646  axdclem2  8889  fzm1  11747  issubc3  15065  pgpfi  16414  imasrng  17045  prdslmodd  17391  icoopnst  21167  iocopnst  21168  axcontlem4  23939  constr2pth  24265  el2wlksotot  24544  nvmdi  25207  mdsl3  26897  elicc3  29699  fzadd2  29824  iscringd  29986  erngdvlem3  35661  erngdvlem3-rN  35669  dvalveclem  35697  dvhlveclem  35780
  Copyright terms: Public domain W3C validator