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  17840  chnub  18776  mhmmnd  19254  rhmqusnsg  21561  ssdifidllem  21620  ssdifidlprm  21622  scmatscm  22808  cfilucfil  24858  2sqmo  27746  tgsegconeu  28931  tgbtwnconn1  29020  legso  29044  footexALT  29175  opphl  29212  trgcopy  29293  zerocgra  29313  dfcgra2  29320  ragcgra  29325  tgaaddcpbllem1  29331  cgrg3col4  29354  cgraer  29359  cgrabasimass  29360  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  angmgmaddrid  29375  prlngex  29411  prlngmolem2  29413  f1otrg  29430  2ndresdju  33225  cyc3genpm  33695  cyc3conja  33700  rloccring  33814  rhmquskerlem  33957  rhmimaidl  33964  mxidlirredi  33978  ssmxidllem  33980  1arithidom  34051  1arithufdlem3  34060  r1plmhm  34123  r1pquslmic  34124  fldextrspunlsplem  34287  fldext2chn  34342  constrconj  34359  constrfin  34360  constrelextdg2  34361  cos9thpiminplylem2  34397  pstmxmet  34511  signstfvneq0  35184  afsval  35286  mblfinlem3  38545  mblfinlem4  38546  primrootscoprmpow  43117  aks6d1c2lem4  43145  dffltz  43624  iunconnlem2  45876  suplesup  46295  limclner  46605  fourierdlem51  47111  hoidmvle  47554  smfmullem3  47747  chnerlem1  47836  upfval  50228