MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-6r Structured version   Visualization version   GIF version

Theorem simp-6r 788
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
Assertion
Ref Expression
simp-6r (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem simp-6r
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21ad6antlr 737 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  catass  17060  mhmmnd  18339  scmatscm  21264  cfilucfil  23312  2sqmo  26173  istrkgb  26401  istrkge  26403  tgbtwnconn1  26521  legso  26545  footexALT  26664  opphl  26700  trgcopy  26750  dfcgra2  26776  cgrg3col4  26799  f1otrg  26817  2ndresdju  30560  cyc3genpm  30996  cyc3conja  31001  rhmimaidl  31181  ssmxidllem  31213  pstmxmet  31419  signstfvneq0  32121  afsval  32221  mblfinlem3  35439  mblfinlem4  35440  dffltz  40043  iunconnlem2  42093  suplesup  42416  limclner  42734  fourierdlem51  43240  hoidmvle  43680  smfmullem3  43866
  Copyright terms: Public domain W3C validator