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

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

Proof of Theorem simp-8r
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21ad8antlr 741 1 (((((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  2sqmo  27496  legso  28622  opphl  28777  f1otrg  28894  2ndresdju  32666  chnso  32988  cyc3conja  33160  rloccring  33257  ssdifidlprm  33466  mxidlprm  33478  mxidlirred  33480  constrconj  33750  constrfin  33751  constrelextdg2  33752  qtophaus  33797  esumcst  34044  dffltz  42621  smfmullem3  46749
  Copyright terms: Public domain W3C validator