Theorem 3anassrs 1358

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 1352	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
3	2	imp41 425	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ralrimivvva  3115  euotd  5421  dfgrp3e  18590  kerf1ghm  19902  psgndif  20719  neiptopnei  22191  neitr  22239  neitx  22666  cnextcn  23126  utoptop  23294  ustuqtoplem  23299  ustuqtop1  23301  utopsnneiplem  23307  utop3cls  23311  neipcfilu  23356  xmetpsmet  23409  metustsym  23617  grporcan  28781  disjdsct  30937  xrofsup  30992  omndmul2  31240  archirngz  31345  archiabllem1  31349  archiabllem2c  31351  reofld  31446  prmidl2  31518  pstmfval  31748  tpr2rico  31764  esumpcvgval  31946  esumcvg  31954  esum2d  31961  voliune  32097  signsply0  32430  signstfvneq0  32451