Theorem simp-6r 787

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  catass  17596  chnub  18532  mhmmnd  18981  rhmqusnsg  21226  scmatscm  22431  cfilucfil  24477  2sqmo  27378  tgbtwnconn1  28556  legso  28580  footexALT  28699  opphl  28735  trgcopy  28785  dfcgra2  28811  cgrg3col4  28834  f1otrg  28852  2ndresdju  32635  cyc3genpm  33130  cyc3conja  33135  rloccring  33246  rhmquskerlem  33399  rhmimaidl  33406  ssdifidllem  33430  ssdifidlprm  33432  mxidlirredi  33445  ssmxidllem  33447  1arithidom  33511  1arithufdlem3  33520  r1plmhm  33579  r1pquslmic  33580  fldextrspunlsplem  33709  fldext2chn  33764  constrconj  33781  constrfin  33782  constrelextdg2  33783  cos9thpiminplylem2  33819  pstmxmet  33933  signstfvneq0  34608  afsval  34707  mblfinlem3  37722  mblfinlem4  37723  primrootscoprmpow  42215  aks6d1c2lem4  42243  dffltz  42755  iunconnlem2  45054  suplesup  45465  limclner  45776  fourierdlem51  46282  hoidmvle  46725  smfmullem3  46918  chnerlem1  47007  upfval  49304