Theorem simp-7r 801

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  catass  17732  isprmidlc  21434  ssdifidlprm  21446  2sqmo  27559  tgbtwnconn1  28802  legso  28826  miriso  28901  footexALT  28949  footex  28952  opphl  28985  lnopp2hpgb  28994  f1otrg  29129  2ndresdju  32906  cyc3genpm  33385  cyc3conja  33390  rloccring  33504  mxidlprm  33670  qsdrngi  33694  1arithidom  33744  fldext2chn  34035  constrconj  34052  constrfin  34053  constrelextdg2  34054  zarcmplem  34188  afsval  34978  dffltz  43228  smfmullem3  47365  chnerlem1  47456