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

Theorem 3adantr2 1148
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 986 . 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 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:  3adant3r2  1197  po3nr  4650  sornom  8438  axdclem2  8681  fzm1  11532  issubc3  14751  pgpfi  16095  imasrng  16699  prdslmodd  17027  icoopnst  20486  iocopnst  20487  axcontlem4  23164  constr2pth  23451  nvmdi  23981  mdsl3  25671  elicc3  28465  fzadd2  28590  iscringd  28752  el2wlksotot  30354  erngdvlem3  34474  erngdvlem3-rN  34482  dvalveclem  34510  dvhlveclem  34593
  Copyright terms: Public domain W3C validator