MPE Home 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 397
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 398
This theorem is referenced by:  catass  17630  2sqmo  26940  tgbtwnconn1  27826  legso  27850  miriso  27921  footexALT  27969  footex  27972  opphl  28005  lnopp2hpgb  28014  f1otrg  28122  2ndresdju  31874  cyc3genpm  32311  cyc3conja  32316  isprmidlc  32566  mxidlprm  32586  qsdrngi  32609  zarcmplem  32861  afsval  33683  dffltz  41376  smfmullem3  45509
  Copyright terms: Public domain W3C validator