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 786
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 735 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ghmcmn  19699  ustuqtop2  23747  ustuqtop4  23749  cnheibor  24471  miriso  27921  f1otrg  28122  txomap  32814  pstmxmet  32877  omssubadd  33299  signstfvneq0  33583  iunconnlem2  43696  suplesup  44049  limcleqr  44360  0ellimcdiv  44365  limclner  44367  fourierdlem51  44873  smflimlem2  45488
  Copyright terms: Public domain W3C validator