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  6936  isf32lem9  8167  axdc3lem4  8259  tskun  8587  dvdscmulr  12798  divalglem8  12840  divscrng  16231  dvfsumlem3  19772  dvfsumrlim  19775  dvfsumrlim2  19776  dvfsumrlim3  19777  dchrisumlem3  21045  dchrisum  21046  abvcxp  21169  padicabv  21184  hvmulcan  22415  hasheuni  24264  pellex  26582  refsumcn  27362  fmuldfeq  27374  stoweidlem31  27441  stoweidlem43  27453  stoweidlem46  27456  stoweidlem52  27462  stoweidlem53  27463  stoweidlem54  27464  stoweidlem55  27465  stoweidlem56  27466  stoweidlem57  27467  stoweidlem58  27468  stoweidlem59  27469  stoweidlem60  27470  stoweidlem62  27472  stoweid  27473  tendoicl  30961  cdlemkfid2N  31088  erngdvlem4  31156  dihmeet  31509
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