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

Theorem 3adantr2 1117
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 955 . 2  |-  ( ( ps  /\  ta  /\  ch )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 461 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3adant3r2  1163  po3nr  4509  sornom  8149  axdclem2  8392  fzm1  11119  issubc3  14038  joinle  14442  pgpfi  15231  imasrng  15717  prdslmodd  16037  icoopnst  18956  iocopnst  18957  constr2pth  21593  nvmdi  22123  mdsl3  23811  axcontlem4  25898  elicc3  26311  fzadd2  26436  iscringd  26600  el2wlksotot  28302  erngdvlem3  31724  erngdvlem3-rN  31732  dvalveclem  31760  dvhlveclem  31843
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator