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  17866  chnub  18802  mhmmnd  19280  rhmqusnsg  21587  ssdifidllem  21646  ssdifidlprm  21648  scmatscm  22834  cfilucfil  24884  2sqmo  27770  tgsegconeu  28955  tgbtwnconn1  29044  legso  29068  footexALT  29199  opphl  29236  trgcopy  29317  zerocgra  29337  dfcgra2  29344  ragcgra  29349  tgaaddcpbllem1  29355  cgrg3col4  29378  cgraer  29383  cgrabasimass  29384  angmgmaddcpbl  29396  angmgmaddcl  29397  angmgmaddlid  29398  angmgmaddrid  29399  prlngex  29435  prlngmolem2  29437  f1otrg  29454  2ndresdju  33291  cyc3genpm  33760  cyc3conja  33765  rloccring  33879  rhmquskerlem  34022  rhmimaidl  34029  mxidlirredi  34043  ssmxidllem  34045  1arithidom  34116  1arithufdlem3  34125  r1plmhm  34188  r1pquslmic  34189  fldextrspunlsplem  34352  fldext2chn  34407  constrconj  34424  constrfin  34425  constrelextdg2  34426  cos9thpiminplylem2  34462  pstmxmet  34576  signstfvneq0  35248  afsval  35350  mblfinlem3  38671  mblfinlem4  38672  primrootscoprmpow  43243  aks6d1c2lem4  43271  dffltz  43764  iunconnlem2  46011  suplesup  46445  limclner  46755  fourierdlem51  47261  hoidmvle  47704  smfmullem3  47897  chnerlem1  47986  upfval  50386