Theorem simp-6l 798

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-6l	⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)

Proof of Theorem simp-6l

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad6antr 748	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ghmcmn  19902  ustuqtop2  24380  ustuqtop4  24382  cnheibor  25095  miriso  28928  f1otrg  29201  txomap  34205  pstmxmet  34268  omssubadd  34671  signstfvneq0  34940  iunconnlem2  45626  suplesup  46038  limcleqr  46341  0ellimcdiv  46346  limclner  46348  fourierdlem51  46854  smflimlem2  47469  upfval  49937