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  3191  euotd  5493  dfgrp3e  19028  kerf1ghm  19235  psgndif  21567  neiptopnei  23075  neitr  23123  neitx  23550  cnextcn  24010  utoptop  24178  ustuqtoplem  24183  ustuqtop1  24185  utopsnneiplem  24191  utop3cls  24195  neipcfilu  24239  xmetpsmet  24292  metustsym  24499  grporcan  30504  disjdsct  32685  xrofsup  32749  omndmul2  33085  archirngz  33192  archiabllem1  33196  archiabllem2c  33198  reofld  33364  prmidl2  33461  pstmfval  33932  tpr2rico  33948  esumpcvgval  34114  esumcvg  34122  esum2d  34129  voliune  34265  signsply0  34588  signstfvneq0  34609  f1o2d2  42251