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 776
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 720 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  simp-7lOLD  781  ghmcmn  18444  ustuqtop2  22266  ustuqtop4  22268  cnheibor  22974  miriso  25786  f1otrg  25972  txomap  30241  pstmxmet  30280  omssubadd  30702  signstfvneq0  30989  iunconnlem2  39693  suplesup  40068  limcleqr  40391  0ellimcdiv  40396  limclner  40398  fourierdlem51  40888  smflimlem2  41497
  Copyright terms: Public domain W3C validator