Theorem 3anassrs 1362

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

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

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 1089

This theorem is referenced by:  ralrimivvva  3184  euotd  5461  dfgrp3e  19007  kerf1ghm  19213  omndmul2  20099  psgndif  21592  neiptopnei  23107  neitr  23155  neitx  23582  cnextcn  24042  utoptop  24209  ustuqtoplem  24214  ustuqtop1  24216  utopsnneiplem  24222  utop3cls  24226  neipcfilu  24270  xmetpsmet  24323  metustsym  24530  grporcan  30604  disjdsct  32791  xrofsup  32855  archirngz  33265  archiabllem1  33269  archiabllem2c  33271  reofld  33418  prmidl2  33516  pstmfval  34056  tpr2rico  34072  esumpcvgval  34238  esumcvg  34246  esum2d  34253  voliune  34389  signsply0  34711  signstfvneq0  34732  f1o2d2  42688