Theorem 3anassrs 1362

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

Step	Hyp	Ref	Expression
1		3anassrs.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
2	1	3exp2 1356	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
3	2	imp41 425	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ralrimivvva  3183  euotd  5467  dfgrp3e  19016  kerf1ghm  19222  omndmul2  20108  psgndif  21582  neiptopnei  23097  neitr  23145  neitx  23572  cnextcn  24032  utoptop  24199  ustuqtoplem  24204  ustuqtop1  24206  utopsnneiplem  24212  utop3cls  24216  neipcfilu  24260  xmetpsmet  24313  metustsym  24520  grporcan  30589  disjdsct  32776  xrofsup  32840  archirngz  33250  archiabllem1  33254  archiabllem2c  33256  reofld  33403  prmidl2  33501  pstmfval  34040  tpr2rico  34056  esumpcvgval  34222  esumcvg  34230  esum2d  34237  voliune  34373  signsply0  34695  signstfvneq0  34716  f1o2d2  42674