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

Theorem simp-6l 809
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 807 . 2 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
21adantr 481 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  simp-7l  811  ghmcmn  18218  ustuqtop2  22027  ustuqtop4  22029  cnheibor  22735  miriso  25546  f1otrg  25732  txomap  29875  pstmxmet  29914  omssubadd  30336  signstfvneq0  30623  iunconnlem2  38991  suplesup  39368  limcleqr  39676  0ellimcdiv  39681  limclner  39683  fourierdlem51  40137  smflimlem2  40743
  Copyright terms: Public domain W3C validator