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  3209  euotd  5486  mpof1o2d  8135  dfgrp3e  19243  kerf1ghm  19454  omndmul2  20340  prmidl2  21615  psgndif  21901  neiptopnei  23443  neitr  23491  neitx  23919  cnextcn  24379  utoptop  24546  ustuqtoplem  24551  ustuqtop1  24553  utopsnneiplem  24559  utop3cls  24563  neipcfilu  24607  xmetpsmet  24660  metustsym  24867  grporcan  31113  disjdsct  33289  xrofsup  33352  archirngz  33743  archiabllem1  33747  archiabllem2c  33749  reofld  33897  pstmfval  34521  tpr2rico  34537  esumpcvgval  34703  esumcvg  34711  esum2d  34718  voliune  34855  signsply0  35173  signstfvneq0  35194