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

Theorem 3anassrs 1173
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
3anassrs.1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Assertion
Ref Expression
3anassrs  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )

Proof of Theorem 3anassrs
StepHypRef Expression
1 3anassrs.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
213exp2 1169 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
32imp41 576 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  disjdsct  23291  xrofsup  23324  kerf1hrm  23428  neiptopnei  23445  tpr2rico  23466  cnextcn  23504  utoptop  23538  ustuqtoplem  23543  ustuqtop1  23545  utopsnneiplem  23551  metustsym  23599  esumpcvgval  23734  esumcvg  23742  voliune  23849
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