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

Theorem 3anassrs 1218
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 1214 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
32imp41 593 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  ralrimivvva  2886  euotd  4748  kerf1hrm  17192  psgndif  18433  neiptopnei  19427  neitr  19475  neitx  19871  cnextcn  20330  utoptop  20500  ustuqtoplem  20505  ustuqtop1  20507  utopsnneiplem  20513  utop3cls  20517  trcfilu  20560  neipcfilu  20562  xmetpsmet  20614  metustsymOLD  20827  metustsym  20828  grporcan  24927  disjdsct  27221  xrofsup  27278  omndmul2  27392  archirngz  27423  archiabllem1  27427  archiabllem2c  27429  reofld  27521  pstmfval  27539  tpr2rico  27558  esumpcvgval  27752  esumcvg  27760  voliune  27869  signsply0  28176  signstfvneq0  28197
  Copyright terms: Public domain W3C validator