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

Theorem 3anassrs 1175
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 1171 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
32imp41 577 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ralrimivvva  2735  euotd  4391  neiptopnei  17112  neitr  17159  neitx  17553  cnextcn  18012  utoptop  18178  ustuqtoplem  18183  ustuqtop1  18185  utopsnneiplem  18191  utop3cls  18195  trcfilu  18238  neipcfilu  18240  metustsym  18468  grporcan  21650  disjdsct  23924  xrofsup  23955  kerf1hrm  24071  reofld  24089  tpr2rico  24107  esumpcvgval  24257  esumcvg  24265  voliune  24372
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