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 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-6r (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem simp-6r
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21ad6antlr 734 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  catass  17395  mhmmnd  18697  scmatscm  21662  cfilucfil  23715  2sqmo  26585  istrkgb  26816  istrkge  26818  tgbtwnconn1  26936  legso  26960  footexALT  27079  opphl  27115  trgcopy  27165  dfcgra2  27191  cgrg3col4  27214  f1otrg  27232  2ndresdju  30986  cyc3genpm  31419  cyc3conja  31424  rhmimaidl  31609  ssmxidllem  31641  pstmxmet  31847  signstfvneq0  32551  afsval  32651  mblfinlem3  35816  mblfinlem4  35817  dffltz  40471  iunconnlem2  42555  suplesup  42878  limclner  43192  fourierdlem51  43698  hoidmvle  44138  smfmullem3  44327
  Copyright terms: Public domain W3C validator