Theorem simp-7r 802

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad7antlr 752	1 ⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  catass  17767  isprmidlc  21509  ssdifidlprm  21523  2sqmo  27638  tgbtwnconn1  28881  legso  28905  miriso  28984  footexALT  29035  footex  29038  opphl  29072  lnopp2hpgb  29082  prlngmolem2  29240  f1otrg  29257  2ndresdju  33031  cyc3genpm  33503  cyc3conja  33508  rloccring  33622  mxidlprm  33784  qsdrngi  33808  1arithidom  33858  fldext2chn  34149  constrconj  34166  constrfin  34167  constrelextdg2  34168  zarcmplem  34302  afsval  35093  dffltz  43407  smfmullem3  47548  chnerlem1  47639