Theorem 3anassrs 1360

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ralrimivvva  3204  euotd  5517  dfgrp3e  19059  kerf1ghm  19266  psgndif  21621  neiptopnei  23141  neitr  23189  neitx  23616  cnextcn  24076  utoptop  24244  ustuqtoplem  24249  ustuqtop1  24251  utopsnneiplem  24257  utop3cls  24261  neipcfilu  24306  xmetpsmet  24359  metustsym  24569  grporcan  30538  disjdsct  32713  xrofsup  32772  omndmul2  33090  archirngz  33197  archiabllem1  33201  archiabllem2c  33203  reofld  33373  prmidl2  33470  pstmfval  33896  tpr2rico  33912  esumpcvgval  34080  esumcvg  34088  esum2d  34095  voliune  34231  signsply0  34567  signstfvneq0  34588  f1o2d2  42274