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  17592  chnub  18528  mhmmnd  18977  rhmqusnsg  21223  scmatscm  22429  cfilucfil  24475  2sqmo  27376  tgbtwnconn1  28554  legso  28578  footexALT  28697  opphl  28733  trgcopy  28783  dfcgra2  28809  cgrg3col4  28832  f1otrg  28850  2ndresdju  32629  cyc3genpm  33119  cyc3conja  33124  rloccring  33235  rhmquskerlem  33388  rhmimaidl  33395  ssdifidllem  33419  ssdifidlprm  33421  mxidlirredi  33434  ssmxidllem  33436  1arithidom  33500  1arithufdlem3  33509  r1plmhm  33568  r1pquslmic  33569  fldextrspunlsplem  33684  fldext2chn  33739  constrconj  33756  constrfin  33757  constrelextdg2  33758  cos9thpiminplylem2  33794  pstmxmet  33908  signstfvneq0  34583  afsval  34682  mblfinlem3  37705  mblfinlem4  37706  primrootscoprmpow  42138  aks6d1c2lem4  42166  dffltz  42673  iunconnlem2  44973  suplesup  45384  limclner  45695  fourierdlem51  46201  hoidmvle  46644  smfmullem3  46837  upfval  49214