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  3178  euotd  5448  dfgrp3e  18948  kerf1ghm  19154  omndmul2  20040  psgndif  21534  neiptopnei  23042  neitr  23090  neitx  23517  cnextcn  23977  utoptop  24144  ustuqtoplem  24149  ustuqtop1  24151  utopsnneiplem  24157  utop3cls  24161  neipcfilu  24205  xmetpsmet  24258  metustsym  24465  grporcan  30490  disjdsct  32676  xrofsup  32742  archirngz  33150  archiabllem1  33154  archiabllem2c  33156  reofld  33300  prmidl2  33398  pstmfval  33901  tpr2rico  33917  esumpcvgval  34083  esumcvg  34091  esum2d  34098  voliune  34234  signsply0  34556  signstfvneq0  34577  f1o2d2  42266