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

Proof of Theorem simp-7r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad7antlr 737	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  17629  2sqmo  26937  tgbtwnconn1  27823  legso  27847  miriso  27918  footexALT  27966  footex  27969  opphl  28002  lnopp2hpgb  28011  f1otrg  28119  2ndresdju  31869  cyc3genpm  32306  cyc3conja  32311  isprmidlc  32561  mxidlprm  32581  qsdrngi  32604  zarcmplem  32856  afsval  33678  dffltz  41377  smfmullem3  45499