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

Theorem 3anassrs 1219
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 1215 . 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 974
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 976
This theorem is referenced by:  ralrimivvva  2865  euotd  4738  kerf1hrm  17371  psgndif  18616  neiptopnei  19611  neitr  19659  neitx  20086  cnextcn  20545  utoptop  20715  ustuqtoplem  20720  ustuqtop1  20722  utopsnneiplem  20728  utop3cls  20732  trcfilu  20775  neipcfilu  20777  xmetpsmet  20829  metustsymOLD  21042  metustsym  21043  grporcan  25201  disjdsct  27499  xrofsup  27560  omndmul2  27680  archirngz  27711  archiabllem1  27715  archiabllem2c  27717  reofld  27808  pstmfval  27853  tpr2rico  27872  esumpcvgval  28062  esumcvg  28070  voliune  28179  signsply0  28486  signstfvneq0  28507
  Copyright terms: Public domain W3C validator