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  2759  euotd  4417  neiptopnei  17151  neitr  17198  neitx  17592  cnextcn  18051  utoptop  18217  ustuqtoplem  18222  ustuqtop1  18224  utopsnneiplem  18230  utop3cls  18234  trcfilu  18277  neipcfilu  18279  xmetpsmet  18331  metustsymOLD  18544  metustsym  18545  grporcan  21762  disjdsct  24043  xrofsup  24079  kerf1hrm  24215  reofld  24233  pstmfval  24244  tpr2rico  24263  esumpcvgval  24421  esumcvg  24429  voliune  24538
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