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  17610  mhmmnd  18961  rhmqusnsg  21210  scmatscm  22416  cfilucfil  24463  2sqmo  27364  tgbtwnconn1  28538  legso  28562  footexALT  28681  opphl  28717  trgcopy  28767  dfcgra2  28793  cgrg3col4  28816  f1otrg  28834  2ndresdju  32606  chnub  32967  cyc3genpm  33107  cyc3conja  33112  rloccring  33223  rhmquskerlem  33375  rhmimaidl  33382  ssdifidllem  33406  ssdifidlprm  33408  mxidlirredi  33421  ssmxidllem  33423  1arithidom  33487  1arithufdlem3  33496  r1plmhm  33554  r1pquslmic  33555  fldextrspunlsplem  33647  fldext2chn  33697  constrconj  33714  constrfin  33715  constrelextdg2  33716  cos9thpiminplylem2  33752  pstmxmet  33866  signstfvneq0  34542  afsval  34641  mblfinlem3  37641  mblfinlem4  37642  primrootscoprmpow  42075  aks6d1c2lem4  42103  dffltz  42610  iunconnlem2  44911  suplesup  45322  limclner  45636  fourierdlem51  46142  hoidmvle  46585  smfmullem3  46778  upfval  49165