Theorem simp-6r 784

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 733	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 206  df-an 396

This theorem is referenced by:  catass  17312  mhmmnd  18612  scmatscm  21570  cfilucfil  23621  2sqmo  26490  istrkgb  26720  istrkge  26722  tgbtwnconn1  26840  legso  26864  footexALT  26983  opphl  27019  trgcopy  27069  dfcgra2  27095  cgrg3col4  27118  f1otrg  27136  2ndresdju  30887  cyc3genpm  31321  cyc3conja  31326  rhmimaidl  31511  ssmxidllem  31543  pstmxmet  31749  signstfvneq0  32451  afsval  32551  mblfinlem3  35743  mblfinlem4  35744  dffltz  40387  iunconnlem2  42444  suplesup  42768  limclner  43082  fourierdlem51  43588  hoidmvle  44028  smfmullem3  44214