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

Theorem 3adantr2 1165
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 1003 . 2  |-  ( ( ps  /\  ta  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 476 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  3adant3r2  1215  po3nr  4788  sornom  8714  axdclem2  8957  issubc3  15753  funcestrcsetclem9  16032  funcsetcestrclem9  16047  pgpfi  17256  imasring  17846  prdslmodd  18191  icoopnst  21965  iocopnst  21966  axcontlem4  24995  constr2pth  25329  el2wlksotot  25608  usg2wlkonot  25609  usg2wotspth  25610  nvmdi  26269  mdsl3  27967  elicc3  30978  fzadd2  32034  iscringd  32196  erngdvlem3  34526  erngdvlem3-rN  34534  dvalveclem  34562  dvhlveclem  34645  dvmptfprodlem  37759  funcringcsetcALTV2lem9  39666  funcringcsetclem9ALTV  39689
  Copyright terms: Public domain W3C validator