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

Theorem 3anassrs 1175
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 1171 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
32imp41 577 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ralrimivvva  2786  euotd  4444  neiptopnei  17179  neitr  17227  neitx  17622  cnextcn  18081  utoptop  18247  ustuqtoplem  18252  ustuqtop1  18254  utopsnneiplem  18260  utop3cls  18264  trcfilu  18307  neipcfilu  18309  xmetpsmet  18361  metustsymOLD  18574  metustsym  18575  grporcan  21792  disjdsct  24073  xrofsup  24109  kerf1hrm  24245  reofld  24263  pstmfval  24274  tpr2rico  24293  esumpcvgval  24451  esumcvg  24459  voliune  24568
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator