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 810
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
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21ad6antr 733 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  simp-7lOLD  815  ghmcmn  18551  ustuqtop2  22373  ustuqtop4  22375  cnheibor  23081  miriso  25920  f1otrg  26107  txomap  30416  pstmxmet  30455  omssubadd  30877  signstfvneq0  31167  iunconnlem2  39926  suplesup  40294  limcleqr  40615  0ellimcdiv  40620  limclner  40622  fourierdlem51  41112  smflimlem2  41721
  Copyright terms: Public domain W3C validator