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

Theorem 3adantr2 1118
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 956 . 2  |-  ( ( ps  /\  ta  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 462 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3adant3r2  1164  po3nr  4520  sornom  8162  axdclem2  8405  fzm1  11132  issubc3  14051  joinle  14455  pgpfi  15244  imasrng  15730  prdslmodd  16050  icoopnst  18969  iocopnst  18970  constr2pth  21606  nvmdi  22136  mdsl3  23824  axcontlem4  25911  elicc3  26334  fzadd2  26459  iscringd  26623  el2wlksotot  28414  erngdvlem3  31861  erngdvlem3-rN  31869  dvalveclem  31897  dvhlveclem  31980
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator