Theorem simp-6l 806

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

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

Proof of Theorem simp-6l

Step	Hyp	Ref	Expression
1		simp-5l 804	. 2 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
2	1	adantr 480	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simp-7l  808  ghmcmn  18060  ustuqtop2  21856  ustuqtop4  21858  cnheibor  22562  miriso  25365  f1otrg  25551  txomap  29229  pstmxmet  29268  omssubadd  29689  signstfvneq0  29975  iunconlem2  38193  suplesup  38496  limcleqr  38711  0ellimcdiv  38716  limclner  38718  fourierdlem51  39050  smflimlem2  39658