Theorem simp-7r 795

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 745	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 208  df-an 397

This theorem is referenced by:  catass  17643  2sqmo  27418  tgbtwnconn1  28661  legso  28685  miriso  28756  footexALT  28804  footex  28807  opphl  28840  lnopp2hpgb  28849  f1otrg  28957  2ndresdju  32741  cyc3genpm  33233  cyc3conja  33238  rloccring  33351  isprmidlc  33530  ssdifidlprm  33541  mxidlprm  33553  qsdrngi  33578  1arithidom  33620  fldext2chn  33912  constrconj  33929  constrfin  33930  constrelextdg2  33931  zarcmplem  34065  afsval  34855  dffltz  43084  smfmullem3  47236  chnerlem1  47327