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

Theorem 3adant1r 1175
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant1r  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3adant1r
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1152 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 695 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1147 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3adant2r  1177  3adant3r  1179  ecopovtrn  6804  isf32lem9  8032  axdc3lem4  8124  tskun  8453  dvdscmulr  12604  divalglem8  12646  divscrng  16041  dvfsumlem3  19428  dvfsumrlim  19431  dvfsumrlim2  19432  dvfsumrlim3  19433  dchrisumlem3  20693  dchrisum  20694  abvcxp  20817  padicabv  20832  hvmulcan  21706  hasheuni  23651  pellex  26068  stoweidlem62  26959  tendoicl  30803  cdlemkfid2N  30930  erngdvlem4  30998  dihmeet  31351
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator