Theorem simp-6r 788

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  17729  mhmmnd  19082  rhmqusnsg  21295  scmatscm  22519  cfilucfil  24572  2sqmo  27481  tgbtwnconn1  28583  legso  28607  footexALT  28726  opphl  28762  trgcopy  28812  dfcgra2  28838  cgrg3col4  28861  f1otrg  28879  2ndresdju  32659  chnub  33002  cyc3genpm  33172  cyc3conja  33177  rloccring  33274  rhmquskerlem  33453  rhmimaidl  33460  ssdifidllem  33484  ssdifidlprm  33486  mxidlirredi  33499  ssmxidllem  33501  1arithidom  33565  1arithufdlem3  33574  r1plmhm  33630  r1pquslmic  33631  fldextrspunlsplem  33723  fldext2chn  33769  constrconj  33786  constrfin  33787  constrelextdg2  33788  pstmxmet  33896  signstfvneq0  34587  afsval  34686  mblfinlem3  37666  mblfinlem4  37667  primrootscoprmpow  42100  aks6d1c2lem4  42128  dffltz  42644  iunconnlem2  44955  suplesup  45350  limclner  45666  fourierdlem51  46172  hoidmvle  46615  smfmullem3  46808  upfval  48933