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  17647  mhmmnd  18996  rhmqusnsg  21195  scmatscm  22400  cfilucfil  24447  2sqmo  27348  tgbtwnconn1  28502  legso  28526  footexALT  28645  opphl  28681  trgcopy  28731  dfcgra2  28757  cgrg3col4  28780  f1otrg  28798  2ndresdju  32573  chnub  32938  cyc3genpm  33109  cyc3conja  33114  rloccring  33221  rhmquskerlem  33396  rhmimaidl  33403  ssdifidllem  33427  ssdifidlprm  33429  mxidlirredi  33442  ssmxidllem  33444  1arithidom  33508  1arithufdlem3  33517  r1plmhm  33575  r1pquslmic  33576  fldextrspunlsplem  33668  fldext2chn  33718  constrconj  33735  constrfin  33736  constrelextdg2  33737  cos9thpiminplylem2  33773  pstmxmet  33887  signstfvneq0  34563  afsval  34662  mblfinlem3  37653  mblfinlem4  37654  primrootscoprmpow  42087  aks6d1c2lem4  42115  dffltz  42622  iunconnlem2  44924  suplesup  45335  limclner  45649  fourierdlem51  46155  hoidmvle  46598  smfmullem3  46791  upfval  49165