Theorem 3anassrs 1381

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ralrimivvva  3213  euotd  5498  mpof1o2d  8123  dfgrp3e  19130  kerf1ghm  19341  omndmul2  20227  prmidl2  21496  psgndif  21782  neiptopnei  23319  neitr  23367  neitx  23795  cnextcn  24255  utoptop  24422  ustuqtoplem  24427  ustuqtop1  24429  utopsnneiplem  24435  utop3cls  24439  neipcfilu  24483  xmetpsmet  24536  metustsym  24743  grporcan  30917  disjdsct  33095  xrofsup  33158  archirngz  33549  archiabllem1  33553  archiabllem2c  33555  reofld  33703  pstmfval  34326  tpr2rico  34342  esumpcvgval  34508  esumcvg  34516  esum2d  34523  voliune  34660  signsply0  34979  signstfvneq0  35000