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

Theorem 3anassrs 1281
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 1276 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
32imp41 616 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  ralrimivvva  2951  euotd  4888  dfgrp3e  17281  kerf1hrm  18509  psgndif  19709  neiptopnei  20685  neitr  20733  neitx  21159  cnextcn  21620  utoptop  21787  ustuqtoplem  21792  ustuqtop1  21794  utopsnneiplem  21800  utop3cls  21804  trcfilu  21847  neipcfilu  21849  xmetpsmet  21901  metustsym  22108  grporcan  26519  disjdsct  28666  xrofsup  28726  omndmul2  28846  archirngz  28877  archiabllem1  28881  archiabllem2c  28883  reofld  28974  pstmfval  29070  tpr2rico  29089  esumpcvgval  29270  esumcvg  29278  esum2d  29285  voliune  29422  signsply0  29757  signstfvneq0  29778
  Copyright terms: Public domain W3C validator