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

Theorem 3adantr2 1159
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 997 . 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 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  3adant3r2  1209  po3nr  4760  sornom  8691  axdclem2  8934  issubc3  15464  funcestrcsetclem9  15743  funcsetcestrclem9  15758  pgpfi  16951  imasring  17590  prdslmodd  17937  icoopnst  21733  iocopnst  21734  axcontlem4  24699  constr2pth  25032  el2wlksotot  25311  usg2wlkonot  25312  usg2wotspth  25313  nvmdi  25972  mdsl3  27661  elicc3  30558  fzadd2  31529  iscringd  31691  erngdvlem3  34022  erngdvlem3-rN  34030  dvalveclem  34058  dvhlveclem  34141  dvmptfprodlem  37122  funcringcsetcALTV2lem9  38376  funcringcsetclem9ALTV  38399
  Copyright terms: Public domain W3C validator