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

Theorem 3anassrs 1176
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 1172 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
32imp41 578 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  ralrimivvva  2806  euotd  4492  neiptopnei  17234  neitr  17282  neitx  17677  cnextcn  18136  utoptop  18302  ustuqtoplem  18307  ustuqtop1  18309  utopsnneiplem  18315  utop3cls  18319  trcfilu  18362  neipcfilu  18364  xmetpsmet  18416  metustsymOLD  18629  metustsym  18630  grporcan  21847  disjdsct  24125  xrofsup  24161  kerf1hrm  24297  reofld  24315  pstmfval  24326  tpr2rico  24345  esumpcvgval  24503  esumcvg  24511  voliune  24620
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator