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

Theorem 3adant1r 1175
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 1152 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 695 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1147 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3adant2r  1177  3adant3r  1179  ecopovtrn  6761  isf32lem9  7987  axdc3lem4  8079  tskun  8408  dvdscmulr  12557  divalglem8  12599  divscrng  15992  dvfsumlem3  19375  dvfsumrlim  19378  dvfsumrlim2  19379  dvfsumrlim3  19380  dchrisumlem3  20640  dchrisum  20641  abvcxp  20764  padicabv  20779  hvmulcan  21651  hasheuni  23453  pellex  26920  stoweidlem62  27811  tendoicl  30985  cdlemkfid2N  31112  erngdvlem4  31180  dihmeet  31533
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator