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  17780  chnub  18716  mhmmnd  19193  rhmqusnsg  21494  ssdifidllem  21553  ssdifidlprm  21555  scmatscm  22741  cfilucfil  24791  2sqmo  27681  tgsegconeu  28836  tgbtwnconn1  28925  legso  28949  footexALT  29080  opphl  29117  trgcopy  29198  zerocgra  29218  dfcgra2  29225  ragcgra  29230  tgaaddcpbllem1  29236  cgrg3col4  29259  cgraer  29264  cgrabasimass  29265  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddlid  29279  angmgmaddrid  29280  prlngex  29316  prlngmolem2  29318  f1otrg  29335  2ndresdju  33130  cyc3genpm  33600  cyc3conja  33605  rloccring  33719  rhmquskerlem  33861  rhmimaidl  33868  mxidlirredi  33882  ssmxidllem  33884  1arithidom  33955  1arithufdlem3  33964  r1plmhm  34027  r1pquslmic  34028  fldextrspunlsplem  34191  fldext2chn  34246  constrconj  34263  constrfin  34264  constrelextdg2  34265  cos9thpiminplylem2  34301  pstmxmet  34415  signstfvneq0  35088  afsval  35190  mblfinlem3  38416  mblfinlem4  38417  primrootscoprmpow  42973  aks6d1c2lem4  43001  dffltz  43488  iunconnlem2  45765  suplesup  46177  limclner  46487  fourierdlem51  46993  hoidmvle  47436  smfmullem3  47629  chnerlem1  47718  upfval  50110