Theorem 3anassrs 1379

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

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

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 1103

This theorem is referenced by:  ralrimivvva  3217  euotd  5494  mpof1o2d  8117  dfgrp3e  19102  kerf1ghm  19313  omndmul2  20199  prmidl2  21433  psgndif  21717  neiptopnei  23254  neitr  23302  neitx  23729  cnextcn  24189  utoptop  24356  ustuqtoplem  24361  ustuqtop1  24363  utopsnneiplem  24369  utop3cls  24373  neipcfilu  24417  xmetpsmet  24470  metustsym  24677  grporcan  30807  disjdsct  32985  xrofsup  33049  archirngz  33446  archiabllem1  33450  archiabllem2c  33452  reofld  33602  pstmfval  34227  tpr2rico  34243  esumpcvgval  34409  esumcvg  34417  esum2d  34424  voliune  34560  signsply0  34879  signstfvneq0  34900