Theorem simp-6r 786

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 735	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  16951  mhmmnd  18215  scmatscm  21116  cfilucfil  23163  2sqmo  26007  istrkgb  26235  istrkge  26237  tgbtwnconn1  26355  legso  26379  footexALT  26498  opphl  26534  trgcopy  26584  dfcgra2  26610  cgrg3col4  26633  f1otrg  26651  cyc3genpm  30789  cyc3conja  30794  ssmxidllem  30973  pstmxmet  31132  signstfvneq0  31837  afsval  31937  mblfinlem3  34925  mblfinlem4  34926  dffltz  39264  iunconnlem2  41262  suplesup  41599  limclner  41924  fourierdlem51  42435  hoidmvle  42875  smfmullem3  43061