Theorem 3anassrs 1282

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ralrimivvva  2955  euotd  4900  dfgrp3e  17338  kerf1hrm  18566  psgndif  19767  neiptopnei  20746  neitr  20794  neitx  21220  cnextcn  21681  utoptop  21848  ustuqtoplem  21853  ustuqtop1  21855  utopsnneiplem  21861  utop3cls  21865  trcfilu  21908  neipcfilu  21910  xmetpsmet  21963  metustsym  22170  grporcan  26756  disjdsct  28863  xrofsup  28923  omndmul2  29043  archirngz  29074  archiabllem1  29078  archiabllem2c  29080  reofld  29171  pstmfval  29267  tpr2rico  29286  esumpcvgval  29467  esumcvg  29475  esum2d  29482  voliune  29619  signsply0  29954  signstfvneq0  29975