Theorem 3anassrs 1359

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  ralrimivvva  3127  euotd  5427  dfgrp3e  18675  kerf1ghm  19987  psgndif  20807  neiptopnei  22283  neitr  22331  neitx  22758  cnextcn  23218  utoptop  23386  ustuqtoplem  23391  ustuqtop1  23393  utopsnneiplem  23399  utop3cls  23403  neipcfilu  23448  xmetpsmet  23501  metustsym  23711  grporcan  28880  disjdsct  31035  xrofsup  31090  omndmul2  31338  archirngz  31443  archiabllem1  31447  archiabllem2c  31449  reofld  31544  prmidl2  31616  pstmfval  31846  tpr2rico  31862  esumpcvgval  32046  esumcvg  32054  esum2d  32061  voliune  32197  signsply0  32530  signstfvneq0  32551