Theorem 3anassrs 1360

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 1354	. 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  3192  euotd  5498  dfgrp3e  19028  kerf1ghm  19235  psgndif  21575  neiptopnei  23087  neitr  23135  neitx  23562  cnextcn  24022  utoptop  24190  ustuqtoplem  24195  ustuqtop1  24197  utopsnneiplem  24203  utop3cls  24207  neipcfilu  24251  xmetpsmet  24304  metustsym  24513  grporcan  30466  disjdsct  32648  xrofsup  32713  omndmul2  33033  archirngz  33140  archiabllem1  33144  archiabllem2c  33146  reofld  33312  prmidl2  33409  pstmfval  33870  tpr2rico  33886  esumpcvgval  34054  esumcvg  34062  esum2d  34069  voliune  34205  signsply0  34541  signstfvneq0  34562  f1o2d2  42248