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

Theorem 3anassrs 1469
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 1463 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
32imp41 416 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  ralrimivvva  3118  euotd  5133  dfgrp3e  17783  kerf1hrm  19011  psgndif  20220  neiptopnei  21215  neitr  21263  neitx  21689  cnextcn  22149  utoptop  22316  ustuqtoplem  22321  ustuqtop1  22323  utopsnneiplem  22329  utop3cls  22333  trcfilu  22376  neipcfilu  22378  xmetpsmet  22431  metustsym  22638  grporcan  27763  disjdsct  29863  xrofsup  29916  omndmul2  30093  archirngz  30124  archiabllem1  30128  archiabllem2c  30130  reofld  30221  pstmfval  30320  tpr2rico  30339  esumpcvgval  30521  esumcvg  30529  esum2d  30536  voliune  30673  signsply0  31010  signstfvneq0  31031
  Copyright terms: Public domain W3C validator