Theorem simp-6l 792

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ghmcmn  19804  ustuqtop2  24232  ustuqtop4  24234  cnheibor  24947  miriso  28763  f1otrg  28964  txomap  34025  pstmxmet  34088  omssubadd  34491  signstfvneq0  34763  iunconnlem2  45385  suplesup  45791  limcleqr  46094  0ellimcdiv  46099  limclner  46101  fourierdlem51  46607  smflimlem2  47222  upfval  49673