Theorem 3anassrs 1382

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  3212  euotd  5493  mpof1o2d  8174  dfgrp3e  19300  kerf1ghm  19511  omndmul2  20398  prmidl2  21673  psgndif  21963  neiptopnei  23505  neitr  23553  neitx  23981  cnextcn  24441  utoptop  24608  ustuqtoplem  24613  ustuqtop1  24615  utopsnneiplem  24621  utop3cls  24625  neipcfilu  24669  xmetpsmet  24722  metustsym  24929  grporcan  31177  disjdsct  33393  xrofsup  33455  archirngz  33849  archiabllem1  33853  archiabllem2c  33855  reofld  34008  pstmfval  34639  tpr2rico  34655  esumpcvgval  34821  esumcvg  34829  esum2d  34836  voliune  34973  signsply0  35291  signstfvneq0  35312