Theorem 3anassrs 1361

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ralrimivvva  3181  euotd  5468  dfgrp3e  18948  kerf1ghm  19155  psgndif  21487  neiptopnei  22995  neitr  23043  neitx  23470  cnextcn  23930  utoptop  24098  ustuqtoplem  24103  ustuqtop1  24105  utopsnneiplem  24111  utop3cls  24115  neipcfilu  24159  xmetpsmet  24212  metustsym  24419  grporcan  30420  disjdsct  32599  xrofsup  32663  omndmul2  32999  archirngz  33116  archiabllem1  33120  archiabllem2c  33122  reofld  33288  prmidl2  33385  pstmfval  33859  tpr2rico  33875  esumpcvgval  34041  esumcvg  34049  esum2d  34056  voliune  34192  signsply0  34515  signstfvneq0  34536  f1o2d2  42194