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  17654  mhmmnd  19003  rhmqusnsg  21202  scmatscm  22407  cfilucfil  24454  2sqmo  27355  tgbtwnconn1  28509  legso  28533  footexALT  28652  opphl  28688  trgcopy  28738  dfcgra2  28764  cgrg3col4  28787  f1otrg  28805  2ndresdju  32580  chnub  32945  cyc3genpm  33116  cyc3conja  33121  rloccring  33228  rhmquskerlem  33403  rhmimaidl  33410  ssdifidllem  33434  ssdifidlprm  33436  mxidlirredi  33449  ssmxidllem  33451  1arithidom  33515  1arithufdlem3  33524  r1plmhm  33582  r1pquslmic  33583  fldextrspunlsplem  33675  fldext2chn  33725  constrconj  33742  constrfin  33743  constrelextdg2  33744  cos9thpiminplylem2  33780  pstmxmet  33894  signstfvneq0  34570  afsval  34669  mblfinlem3  37660  mblfinlem4  37661  primrootscoprmpow  42094  aks6d1c2lem4  42122  dffltz  42629  iunconnlem2  44931  suplesup  45342  limclner  45656  fourierdlem51  46162  hoidmvle  46605  smfmullem3  46798  upfval  49169