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 430	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ralrimivvva  3211  euotd  5496  mpof1o2d  8117  dfgrp3e  19101  kerf1ghm  19312  omndmul2  20198  prmidl2  21466  psgndif  21752  neiptopnei  23289  neitr  23337  neitx  23764  cnextcn  24224  utoptop  24391  ustuqtoplem  24396  ustuqtop1  24398  utopsnneiplem  24404  utop3cls  24408  neipcfilu  24452  xmetpsmet  24505  metustsym  24712  grporcan  30870  disjdsct  33048  xrofsup  33112  archirngz  33509  archiabllem1  33513  archiabllem2c  33515  reofld  33663  pstmfval  34286  tpr2rico  34302  esumpcvgval  34468  esumcvg  34476  esum2d  34483  voliune  34619  signsply0  34938  signstfvneq0  34959