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

Theorem 3adant1r 1178
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 1155 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 697 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1150 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3adant2r  1180  3adant3r  1182  ecopovtrn  7036  isf32lem9  8272  axdc3lem4  8364  tskun  8692  dvdscmulr  12909  divalglem8  12951  divscrng  16342  dvfsumlem3  19943  dvfsumrlim  19946  dvfsumrlim2  19947  dvfsumrlim3  19948  dchrisumlem3  21216  dchrisum  21217  abvcxp  21340  padicabv  21355  hvmulcan  22605  isarchi2  24286  hasheuni  24506  pellex  26936  refsumcn  27715  fmuldfeq  27727  stoweidlem31  27794  stoweidlem43  27806  stoweidlem46  27809  stoweidlem52  27815  stoweidlem53  27816  stoweidlem54  27817  stoweidlem55  27818  stoweidlem56  27819  stoweidlem57  27820  stoweidlem58  27821  stoweidlem59  27822  stoweidlem60  27823  stoweidlem62  27825  stoweid  27826  tendoicl  31691  cdlemkfid2N  31818  erngdvlem4  31886  dihmeet  32239
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator