Theorem simp-6r 800

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 750	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  catass  17767  chnub  18703  mhmmnd  19161  rhmqusnsg  21462  ssdifidllem  21521  ssdifidlprm  21523  scmatscm  22707  cfilucfil  24753  2sqmo  27638  tgbtwnconn1  28881  legso  28905  footexALT  29035  opphl  29072  trgcopy  29152  dfcgra2  29178  ragcgra  29183  cgrg3col4  29207  prlngex  29238  prlngmolem2  29240  f1otrg  29257  2ndresdju  33031  cyc3genpm  33503  cyc3conja  33508  rloccring  33622  rhmquskerlem  33764  rhmimaidl  33771  mxidlirredi  33785  ssmxidllem  33787  1arithidom  33858  1arithufdlem3  33867  r1plmhm  33930  r1pquslmic  33931  fldextrspunlsplem  34094  fldext2chn  34149  constrconj  34166  constrfin  34167  constrelextdg2  34168  cos9thpiminplylem2  34204  pstmxmet  34318  signstfvneq0  34991  afsval  35093  mblfinlem3  38351  mblfinlem4  38352  primrootscoprmpow  42907  aks6d1c2lem4  42935  dffltz  43407  iunconnlem2  45684  suplesup  46096  limclner  46406  fourierdlem51  46912  hoidmvle  47355  smfmullem3  47548  chnerlem1  47639  upfval  49995