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

Theorem 3anassrs 1209
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 1205 . 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 965
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 967
This theorem is referenced by:  ralrimivvva  2809  euotd  4592  kerf1hrm  16831  psgndif  18032  neiptopnei  18736  neitr  18784  neitx  19180  cnextcn  19639  utoptop  19809  ustuqtoplem  19814  ustuqtop1  19816  utopsnneiplem  19822  utop3cls  19826  trcfilu  19869  neipcfilu  19871  xmetpsmet  19923  metustsymOLD  20136  metustsym  20137  grporcan  23708  disjdsct  25998  xrofsup  26055  omndmul2  26175  archirngz  26206  archiabllem1  26210  archiabllem2c  26212  reofld  26308  pstmfval  26323  tpr2rico  26342  esumpcvgval  26527  esumcvg  26535  voliune  26645  signsply0  26952  signstfvneq0  26973
  Copyright terms: Public domain W3C validator