Theorem simp-6l 786

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 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad6antr 736	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  ghmcmn  19768  ustuqtop2  24137  ustuqtop4  24139  cnheibor  24861  miriso  28604  f1otrg  28805  txomap  33831  pstmxmet  33894  omssubadd  34298  signstfvneq0  34570  iunconnlem2  44931  suplesup  45342  limcleqr  45649  0ellimcdiv  45654  limclner  45656  fourierdlem51  46162  smflimlem2  46777  upfval  49169