Theorem simp-6r 785

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  catass  17395  mhmmnd  18697  scmatscm  21662  cfilucfil  23715  2sqmo  26585  istrkgb  26816  istrkge  26818  tgbtwnconn1  26936  legso  26960  footexALT  27079  opphl  27115  trgcopy  27165  dfcgra2  27191  cgrg3col4  27214  f1otrg  27232  2ndresdju  30986  cyc3genpm  31419  cyc3conja  31424  rhmimaidl  31609  ssmxidllem  31641  pstmxmet  31847  signstfvneq0  32551  afsval  32651  mblfinlem3  35816  mblfinlem4  35817  dffltz  40471  iunconnlem2  42555  suplesup  42878  limclner  43192  fourierdlem51  43698  hoidmvle  44138  smfmullem3  44327