Theorem 3anassrs 1354

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1081

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 399  df-3an 1083

This theorem is referenced by:  ralrimivvva  3190  euotd  5394  dfgrp3e  18191  kerf1ghm  19489  kerf1hrmOLD  19490  psgndif  20738  neiptopnei  21732  neitr  21780  neitx  22207  cnextcn  22667  utoptop  22835  ustuqtoplem  22840  ustuqtop1  22842  utopsnneiplem  22848  utop3cls  22852  neipcfilu  22897  xmetpsmet  22950  metustsym  23157  grporcan  28287  disjdsct  30430  xrofsup  30484  omndmul2  30706  archirngz  30811  archiabllem1  30815  archiabllem2c  30817  reofld  30906  prmidl2  30951  pstmfval  31129  tpr2rico  31148  esumpcvgval  31330  esumcvg  31338  esum2d  31345  voliune  31481  signsply0  31814  signstfvneq0  31835