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

Theorem 3anassrs 1287
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
3anassrs.1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
3anassrs ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3anassrs
StepHypRef Expression
1 3anassrs.1 . . 3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
213exp2 1282 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
32imp41 618 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  ralrimivvva  2968  euotd  4945  dfgrp3e  17455  kerf1hrm  18683  psgndif  19888  neiptopnei  20876  neitr  20924  neitx  21350  cnextcn  21811  utoptop  21978  ustuqtoplem  21983  ustuqtop1  21985  utopsnneiplem  21991  utop3cls  21995  trcfilu  22038  neipcfilu  22040  xmetpsmet  22093  metustsym  22300  grporcan  27260  disjdsct  29364  xrofsup  29418  omndmul2  29539  archirngz  29570  archiabllem1  29574  archiabllem2c  29576  reofld  29667  pstmfval  29763  tpr2rico  29782  esumpcvgval  29963  esumcvg  29971  esum2d  29978  voliune  30115  signsply0  30450  signstfvneq0  30471
  Copyright terms: Public domain W3C validator