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 791
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  27482  legso  28608  opphl  28763  f1otrg  28880  2ndresdju  32660  chnso  33005  cyc3conja  33178  rloccring  33275  ssdifidlprm  33487  mxidlprm  33499  mxidlirred  33501  constrconj  33787  constrfin  33788  constrelextdg2  33789  qtophaus  33836  esumcst  34065  dffltz  42649  smfmullem3  46813
  Copyright terms: Public domain W3C validator