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  3183  euotd  5473  dfgrp3e  18972  kerf1ghm  19179  psgndif  21511  neiptopnei  23019  neitr  23067  neitx  23494  cnextcn  23954  utoptop  24122  ustuqtoplem  24127  ustuqtop1  24129  utopsnneiplem  24135  utop3cls  24139  neipcfilu  24183  xmetpsmet  24236  metustsym  24443  grporcan  30447  disjdsct  32626  xrofsup  32690  omndmul2  33026  archirngz  33143  archiabllem1  33147  archiabllem2c  33149  reofld  33315  prmidl2  33412  pstmfval  33886  tpr2rico  33902  esumpcvgval  34068  esumcvg  34076  esum2d  34083  voliune  34219  signsply0  34542  signstfvneq0  34563  f1o2d2  42221