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 738	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  17643  chnub  18579  mhmmnd  19031  rhmqusnsg  21275  scmatscm  22488  cfilucfil  24534  2sqmo  27414  tgbtwnconn1  28657  legso  28681  footexALT  28800  opphl  28836  trgcopy  28886  dfcgra2  28912  cgrg3col4  28935  f1otrg  28953  2ndresdju  32737  cyc3genpm  33228  cyc3conja  33233  rloccring  33346  rhmquskerlem  33500  rhmimaidl  33507  ssdifidllem  33531  ssdifidlprm  33533  mxidlirredi  33546  ssmxidllem  33548  1arithidom  33612  1arithufdlem3  33621  r1plmhm  33685  r1pquslmic  33686  fldextrspunlsplem  33833  fldext2chn  33888  constrconj  33905  constrfin  33906  constrelextdg2  33907  cos9thpiminplylem2  33943  pstmxmet  34057  signstfvneq0  34732  afsval  34831  mblfinlem3  37994  mblfinlem4  37995  primrootscoprmpow  42552  aks6d1c2lem4  42580  dffltz  43081  iunconnlem2  45379  suplesup  45787  limclner  46097  fourierdlem51  46603  hoidmvle  47046  smfmullem3  47239  chnerlem1  47328  upfval  49663