Theorem 3anassrs 1356

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ralrimivvva  3194  euotd  5405  dfgrp3e  18201  kerf1ghm  19499  kerf1hrmOLD  19500  psgndif  20748  neiptopnei  21742  neitr  21790  neitx  22217  cnextcn  22677  utoptop  22845  ustuqtoplem  22850  ustuqtop1  22852  utopsnneiplem  22858  utop3cls  22862  neipcfilu  22907  xmetpsmet  22960  metustsym  23167  grporcan  28297  disjdsct  30440  xrofsup  30494  omndmul2  30715  archirngz  30820  archiabllem1  30824  archiabllem2c  30826  reofld  30915  prmidl2  30960  pstmfval  31138  tpr2rico  31157  esumpcvgval  31339  esumcvg  31347  esum2d  31354  voliune  31490  signsply0  31823  signstfvneq0  31844