Theorem 3anassrs 1357

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ralrimivvva  3157  euotd  5368  dfgrp3e  18191  kerf1ghm  19491  psgndif  20291  neiptopnei  21737  neitr  21785  neitx  22212  cnextcn  22672  utoptop  22840  ustuqtoplem  22845  ustuqtop1  22847  utopsnneiplem  22853  utop3cls  22857  neipcfilu  22902  xmetpsmet  22955  metustsym  23162  grporcan  28301  disjdsct  30462  xrofsup  30518  omndmul2  30763  archirngz  30868  archiabllem1  30872  archiabllem2c  30874  reofld  30964  prmidl2  31024  pstmfval  31249  tpr2rico  31265  esumpcvgval  31447  esumcvg  31455  esum2d  31462  voliune  31598  signsply0  31931  signstfvneq0  31952