Theorem simp-7r 799

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  catass  17701  2sqmo  27478  tgbtwnconn1  28721  legso  28745  miriso  28816  footexALT  28864  footex  28867  opphl  28900  lnopp2hpgb  28909  f1otrg  29017  2ndresdju  32801  cyc3genpm  33293  cyc3conja  33298  rloccring  33413  isprmidlc  33594  ssdifidlprm  33606  mxidlprm  33619  qsdrngi  33644  1arithidom  33694  fldext2chn  33986  constrconj  34003  constrfin  34004  constrelextdg2  34005  zarcmplem  34139  afsval  34932  dffltz  43180  smfmullem3  47331  chnerlem1  47422