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

Theorem 3anassrs 1454
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 1448 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
32imp41 620 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  ralrimivvva  3110  euotd  5123  dfgrp3e  17716  kerf1hrm  18945  psgndif  20150  neiptopnei  21138  neitr  21186  neitx  21612  cnextcn  22072  utoptop  22239  ustuqtoplem  22244  ustuqtop1  22246  utopsnneiplem  22252  utop3cls  22256  trcfilu  22299  neipcfilu  22301  xmetpsmet  22354  metustsym  22561  grporcan  27681  disjdsct  29789  xrofsup  29842  omndmul2  30021  archirngz  30052  archiabllem1  30056  archiabllem2c  30058  reofld  30149  pstmfval  30248  tpr2rico  30267  esumpcvgval  30449  esumcvg  30457  esum2d  30464  voliune  30601  signsply0  30937  signstfvneq0  30958
  Copyright terms: Public domain W3C validator