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 787
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 736 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  17492  2sqmo  26691  tgbtwnconn1  27225  legso  27249  miriso  27320  footexALT  27368  footex  27371  opphl  27404  lnopp2hpgb  27413  f1otrg  27521  2ndresdju  31273  cyc3genpm  31706  cyc3conja  31711  isprmidlc  31920  mxidlprm  31937  zarcmplem  32129  afsval  32951  dffltz  40733  smfmullem3  44668
  Copyright terms: Public domain W3C validator