Theorem simp-7r 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-7r	⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem simp-7r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad7antlr 735	1 ⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  catass  17634  2sqmo  27176  tgbtwnconn1  28093  legso  28117  miriso  28188  footexALT  28236  footex  28239  opphl  28272  lnopp2hpgb  28281  f1otrg  28389  2ndresdju  32141  cyc3genpm  32581  cyc3conja  32586  isprmidlc  32840  mxidlprm  32860  qsdrngi  32883  zarcmplem  33159  afsval  33981  dffltz  41678  smfmullem3  45807