Theorem 3anassrs 1373

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ralrimivvva  3207  euotd  5479  mpof1o2d  8099  dfgrp3e  19073  kerf1ghm  19278  omndmul2  20164  psgndif  21642  neiptopnei  23180  neitr  23228  neitx  23655  cnextcn  24115  utoptop  24282  ustuqtoplem  24287  ustuqtop1  24289  utopsnneiplem  24295  utop3cls  24299  neipcfilu  24343  xmetpsmet  24396  metustsym  24603  grporcan  30678  disjdsct  32866  xrofsup  32930  archirngz  33330  archiabllem1  33334  archiabllem2c  33336  reofld  33490  prmidl2  33588  pstmfval  34154  tpr2rico  34170  esumpcvgval  34336  esumcvg  34344  esum2d  34351  voliune  34487  signsply0  34806  signstfvneq0  34827