Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-6l Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 simp-5l 804 . 2 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
21adantr 480 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator