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  2801  euotd  4460  neiptopnei  17201  neitr  17249  neitx  17644  cnextcn  18103  utoptop  18269  ustuqtoplem  18274  ustuqtop1  18276  utopsnneiplem  18282  utop3cls  18286  trcfilu  18329  neipcfilu  18331  xmetpsmet  18383  metustsymOLD  18596  metustsym  18597  grporcan  21814  disjdsct  24095  xrofsup  24131  kerf1hrm  24267  reofld  24285  pstmfval  24296  tpr2rico  24315  esumpcvgval  24473  esumcvg  24481  voliune  24590
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