Theorem simp-6r 795

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 745	1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  catass  17690  chnub  18626  mhmmnd  19078  rhmqusnsg  21324  scmatscm  22542  cfilucfil  24588  2sqmo  27467  tgbtwnconn1  28710  legso  28734  footexALT  28853  opphl  28889  trgcopy  28939  dfcgra2  28965  cgrg3col4  28988  f1otrg  29006  2ndresdju  32790  cyc3genpm  33282  cyc3conja  33287  rloccring  33400  rhmquskerlem  33557  rhmimaidl  33564  ssdifidllem  33588  ssdifidlprm  33590  mxidlirredi  33603  ssmxidllem  33605  1arithidom  33677  1arithufdlem3  33686  r1plmhm  33750  r1pquslmic  33751  fldextrspunlsplem  33914  fldext2chn  33969  constrconj  33986  constrfin  33987  constrelextdg2  33988  cos9thpiminplylem2  34024  pstmxmet  34138  signstfvneq0  34813  afsval  34915  mblfinlem3  38096  mblfinlem4  38097  primrootscoprmpow  42654  aks6d1c2lem4  42682  dffltz  43154  iunconnlem2  45448  suplesup  45853  limclner  46163  fourierdlem51  46669  hoidmvle  47112  smfmullem3  47305  chnerlem1  47396  upfval  49735