Theorem 3anassrs 1290

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

Step	Hyp	Ref	Expression
1		3anassrs.1	. . 3 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )
2	1	3exp2 1285	. 2 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
3	2	imp41 619	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  ralrimivvva  2972  euotd  4975  dfgrp3e  17515  kerf1hrm  18743  psgndif  19948  neiptopnei  20936  neitr  20984  neitx  21410  cnextcn  21871  utoptop  22038  ustuqtoplem  22043  ustuqtop1  22045  utopsnneiplem  22051  utop3cls  22055  trcfilu  22098  neipcfilu  22100  xmetpsmet  22153  metustsym  22360  grporcan  27372  disjdsct  29480  xrofsup  29533  omndmul2  29712  archirngz  29743  archiabllem1  29747  archiabllem2c  29749  reofld  29840  pstmfval  29939  tpr2rico  29958  esumpcvgval  30140  esumcvg  30148  esum2d  30155  voliune  30292  signsply0  30628  signstfvneq0  30649