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

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

Proof of Theorem simp-7r
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21ad7antlr 738 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  16957  2sqmo  26024  tgbtwnconn1  26372  legso  26396  miriso  26467  footexALT  26515  footex  26518  opphl  26551  lnopp2hpgb  26560  f1otrg  26668  cyc3genpm  30826  cyc3conja  30831  isprmidlc  31004  mxidlprm  31018  afsval  31999  dffltz  39531  smfmullem3  43351
 Copyright terms: Public domain W3C validator