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 787
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 736 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  ghmcmn  19849  ustuqtop2  24251  ustuqtop4  24253  cnheibor  24987  miriso  28678  f1otrg  28879  txomap  33833  pstmxmet  33896  omssubadd  34302  signstfvneq0  34587  iunconnlem2  44955  suplesup  45350  limcleqr  45659  0ellimcdiv  45664  limclner  45666  fourierdlem51  46172  smflimlem2  46787  upfval  48933
  Copyright terms: Public domain W3C validator