Theorem simp-6l 799

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 749	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)

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

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

This theorem is used by:  ghmcmn  20025  ustuqtop2  24541  ustuqtop4  24543  cnheibor  25256  miriso  29124  f1otrg  29430  txomap  34448  pstmxmet  34511  omssubadd  34915  signstfvneq0  35184  iunconnlem2  45876  suplesup  46295  limcleqr  46598  0ellimcdiv  46603  limclner  46605  fourierdlem51  47111  smflimlem2  47726  upfval  50228