MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant1r Structured version   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  7007  isf32lem9  8241  axdc3lem4  8333  tskun  8661  dvdscmulr  12878  divalglem8  12920  divscrng  16311  dvfsumlem3  19912  dvfsumrlim  19915  dvfsumrlim2  19916  dvfsumrlim3  19917  dchrisumlem3  21185  dchrisum  21186  abvcxp  21309  padicabv  21324  hvmulcan  22574  isarchi2  24255  hasheuni  24475  pellex  26898  refsumcn  27677  fmuldfeq  27689  stoweidlem31  27756  stoweidlem43  27768  stoweidlem46  27771  stoweidlem52  27777  stoweidlem53  27778  stoweidlem54  27779  stoweidlem55  27780  stoweidlem56  27781  stoweidlem57  27782  stoweidlem58  27783  stoweidlem59  27784  stoweidlem60  27785  stoweidlem62  27787  stoweid  27788  tendoicl  31593  cdlemkfid2N  31720  erngdvlem4  31788  dihmeet  32141
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