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

Theorem 3adant1r 1177
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 1154 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 696 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1149 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3adant2r  1179  3adant3r  1181  ecopovtrn  6993  isf32lem9  8225  axdc3lem4  8317  tskun  8645  dvdscmulr  12861  divalglem8  12903  divscrng  16294  dvfsumlem3  19895  dvfsumrlim  19898  dvfsumrlim2  19899  dvfsumrlim3  19900  dchrisumlem3  21168  dchrisum  21169  abvcxp  21292  padicabv  21307  hvmulcan  22557  isarchi2  24238  hasheuni  24458  pellex  26830  refsumcn  27610  fmuldfeq  27622  stoweidlem31  27689  stoweidlem43  27701  stoweidlem46  27704  stoweidlem52  27710  stoweidlem53  27711  stoweidlem54  27712  stoweidlem55  27713  stoweidlem56  27714  stoweidlem57  27715  stoweidlem58  27716  stoweidlem59  27717  stoweidlem60  27718  stoweidlem62  27720  stoweid  27721  tendoicl  31324  cdlemkfid2N  31451  erngdvlem4  31519  dihmeet  31872
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