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  19897  ustuqtop2  24364  ustuqtop4  24366  cnheibor  25079  miriso  28905  f1otrg  29157  txomap  34165  pstmxmet  34228  omssubadd  34631  signstfvneq0  34900  iunconnlem2  45530  suplesup  45942  limcleqr  46245  0ellimcdiv  46250  limclner  46252  fourierdlem51  46758  smflimlem2  47373  upfval  49834