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 785
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 734 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  ghmcmn  18955  ustuqtop2  22854  ustuqtop4  22856  cnheibor  23562  miriso  26459  f1otrg  26660  txomap  31102  pstmxmet  31141  omssubadd  31562  signstfvneq0  31846  iunconnlem2  41275  suplesup  41613  limcleqr  41931  0ellimcdiv  41936  limclner  41938  fourierdlem51  42449  smflimlem2  43055
  Copyright terms: Public domain W3C validator