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 739 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:  catass  17579  2sqmo  27329  tgbtwnconn1  28507  legso  28531  miriso  28602  footexALT  28650  footex  28653  opphl  28686  lnopp2hpgb  28695  f1otrg  28803  2ndresdju  32583  cyc3genpm  33089  cyc3conja  33094  rloccring  33205  isprmidlc  33380  ssdifidlprm  33391  mxidlprm  33403  qsdrngi  33428  1arithidom  33470  fldext2chn  33709  constrconj  33726  constrfin  33727  constrelextdg2  33728  zarcmplem  33862  afsval  34652  dffltz  42624  smfmullem3  46788
  Copyright terms: Public domain W3C validator