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

Theorem 3anassrs 1204
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 1200 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
32imp41 590 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  ralrimivvva  2801  euotd  4582  psgndif  17876  neiptopnei  18580  neitr  18628  neitx  19024  cnextcn  19483  utoptop  19653  ustuqtoplem  19658  ustuqtop1  19660  utopsnneiplem  19666  utop3cls  19670  trcfilu  19713  neipcfilu  19715  xmetpsmet  19767  metustsymOLD  19980  metustsym  19981  grporcan  23533  disjdsct  25824  xrofsup  25880  omndmul2  26001  archirngz  26032  archiabllem1  26036  archiabllem2c  26038  kerf1hrm  26147  reofld  26164  pstmfval  26179  tpr2rico  26198  esumpcvgval  26383  esumcvg  26391  voliune  26501  signsply0  26802  signstfvneq0  26823
  Copyright terms: Public domain W3C validator