Theorem simp-7r 789

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 739	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 207  df-an 396

This theorem is referenced by:  catass  17594  2sqmo  27376  tgbtwnconn1  28554  legso  28578  miriso  28649  footexALT  28697  footex  28700  opphl  28733  lnopp2hpgb  28742  f1otrg  28850  2ndresdju  32633  cyc3genpm  33128  cyc3conja  33133  rloccring  33244  isprmidlc  33419  ssdifidlprm  33430  mxidlprm  33442  qsdrngi  33467  1arithidom  33509  fldext2chn  33762  constrconj  33779  constrfin  33780  constrelextdg2  33781  zarcmplem  33915  afsval  34705  dffltz  42753  smfmullem3  46916  chnerlem1  47005