Theorem 3anassrs 1381

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ralrimivvva  3208  euotd  5485  mpof1o2d  8140  dfgrp3e  19256  kerf1ghm  19467  omndmul2  20353  prmidl2  21628  psgndif  21914  neiptopnei  23456  neitr  23504  neitx  23932  cnextcn  24392  utoptop  24559  ustuqtoplem  24564  ustuqtop1  24566  utopsnneiplem  24572  utop3cls  24576  neipcfilu  24620  xmetpsmet  24673  metustsym  24880  grporcan  31126  disjdsct  33344  xrofsup  33406  archirngz  33797  archiabllem1  33801  archiabllem2c  33803  reofld  33951  pstmfval  34575  tpr2rico  34591  esumpcvgval  34757  esumcvg  34765  esum2d  34772  voliune  34909  signsply0  35227  signstfvneq0  35248