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  6777  isf32lem9  8003  axdc3lem4  8095  tskun  8424  dvdscmulr  12573  divalglem8  12615  divscrng  16008  dvfsumlem3  19391  dvfsumrlim  19394  dvfsumrlim2  19395  dvfsumrlim3  19396  dchrisumlem3  20656  dchrisum  20657  abvcxp  20780  padicabv  20795  hvmulcan  21667  hasheuni  23468  pellex  27023  stoweidlem62  27914  tendoicl  31607  cdlemkfid2N  31734  erngdvlem4  31802  dihmeet  32155
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