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

Theorem 3adant1r 1204
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 1181 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 707 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1176 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  3adant2r  1206  3adant3r  1208  ecopovtrn  7191  isf32lem9  8518  axdc3lem4  8610  tskun  8940  dvdscmulr  13543  divalglem8  13586  divscrng  17243  dvfsumlem3  21341  dvfsumrlim  21344  dvfsumrlim2  21345  dvfsumrlim3  21346  dchrisumlem3  22624  dchrisum  22625  abvcxp  22748  padicabv  22763  hvmulcan  24296  isarchi2  26025  archiabllem2c  26035  hasheuni  26387  pellex  29018  refsumcn  29594  fmuldfeq  29606  stoweidlem31  29669  stoweidlem43  29681  stoweidlem46  29684  stoweidlem52  29690  stoweidlem53  29691  stoweidlem54  29692  stoweidlem55  29693  stoweidlem56  29694  stoweidlem57  29695  stoweidlem58  29696  stoweidlem59  29697  stoweidlem60  29698  stoweidlem62  29700  stoweid  29701  el0ldep  30706  tendoicl  34010  cdlemkfid2N  34137  erngdvlem4  34205
  Copyright terms: Public domain W3C validator