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  2763  euotd  4421  neiptopnei  17155  neitr  17202  neitx  17596  cnextcn  18055  utoptop  18221  ustuqtoplem  18226  ustuqtop1  18228  utopsnneiplem  18234  utop3cls  18238  trcfilu  18281  neipcfilu  18283  xmetpsmet  18335  metustsymOLD  18548  metustsym  18549  grporcan  21766  disjdsct  24047  xrofsup  24083  kerf1hrm  24219  reofld  24237  pstmfval  24248  tpr2rico  24267  esumpcvgval  24425  esumcvg  24433  voliune  24542
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