Theorem simp-6r 797

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 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad6antlr 747	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  catass  17708  chnub  18644  mhmmnd  19096  rhmqusnsg  21342  scmatscm  22560  cfilucfil  24606  2sqmo  27488  tgbtwnconn1  28731  legso  28755  footexALT  28874  opphl  28910  trgcopy  28960  dfcgra2  28986  cgrg3col4  29009  f1otrg  29027  2ndresdju  32811  cyc3genpm  33292  cyc3conja  33297  rloccring  33412  rhmquskerlem  33571  rhmimaidl  33578  ssdifidllem  33603  ssdifidlprm  33605  mxidlirredi  33619  ssmxidllem  33621  1arithidom  33693  1arithufdlem3  33702  r1plmhm  33766  r1pquslmic  33767  fldextrspunlsplem  33930  fldext2chn  33985  constrconj  34002  constrfin  34003  constrelextdg2  34004  cos9thpiminplylem2  34040  pstmxmet  34154  signstfvneq0  34826  afsval  34928  mblfinlem3  38118  mblfinlem4  38119  primrootscoprmpow  42676  aks6d1c2lem4  42704  dffltz  43176  iunconnlem2  45470  suplesup  45875  limclner  46185  fourierdlem51  46691  hoidmvle  47134  smfmullem3  47327  chnerlem1  47418  upfval  49757