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

Theorem 3adant1r 1211
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 1188 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 714 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1183 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  3adant2r  1213  3adant3r  1215  ecopovtrn  7195  isf32lem9  8522  axdc3lem4  8614  tskun  8945  dvdscmulr  13553  divalglem8  13596  divscrng  17299  dvfsumlem3  21475  dvfsumrlim  21478  dvfsumrlim2  21479  dvfsumrlim3  21480  dchrisumlem3  22715  dchrisum  22716  abvcxp  22839  padicabv  22854  hvmulcan  24425  isarchi2  26153  archiabllem2c  26163  hasheuni  26486  pellex  29129  refsumcn  29705  fmuldfeq  29717  stoweidlem31  29779  stoweidlem43  29791  stoweidlem46  29794  stoweidlem52  29800  stoweidlem53  29801  stoweidlem54  29802  stoweidlem55  29803  stoweidlem56  29804  stoweidlem57  29805  stoweidlem58  29806  stoweidlem59  29807  stoweidlem60  29808  stoweidlem62  29810  stoweid  29811  el0ldep  30889  tendoicl  34280  cdlemkfid2N  34407  erngdvlem4  34475
  Copyright terms: Public domain W3C validator