Theorem simp-6r 799

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-6r	⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem simp-6r

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad6antlr 749	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  catass  17743  chnub  18679  mhmmnd  19131  rhmqusnsg  21406  ssdifidllem  21465  ssdifidlprm  21467  scmatscm  22651  cfilucfil  24697  2sqmo  27582  tgbtwnconn1  28825  legso  28849  footexALT  28979  opphl  29016  trgcopy  29096  dfcgra2  29122  ragcgra  29127  cgrg3col4  29151  prlngex  29182  prlngmolem2  29184  f1otrg  29201  2ndresdju  32975  cyc3genpm  33453  cyc3conja  33458  rloccring  33572  rhmquskerlem  33714  rhmimaidl  33721  mxidlirredi  33735  ssmxidllem  33737  1arithidom  33808  1arithufdlem3  33817  r1plmhm  33880  r1pquslmic  33881  fldextrspunlsplem  34044  fldext2chn  34099  constrconj  34116  constrfin  34117  constrelextdg2  34118  cos9thpiminplylem2  34154  pstmxmet  34268  signstfvneq0  34940  afsval  35042  mblfinlem3  38291  mblfinlem4  38292  primrootscoprmpow  42847  aks6d1c2lem4  42875  dffltz  43349  iunconnlem2  45626  suplesup  46038  limclner  46348  fourierdlem51  46854  hoidmvle  47297  smfmullem3  47490  chnerlem1  47581  upfval  49937