Theorem simp-7r 790

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  17729  2sqmo  27481  tgbtwnconn1  28583  legso  28607  miriso  28678  footexALT  28726  footex  28729  opphl  28762  lnopp2hpgb  28771  f1otrg  28879  2ndresdju  32659  cyc3genpm  33172  cyc3conja  33177  rloccring  33274  isprmidlc  33475  ssdifidlprm  33486  mxidlprm  33498  qsdrngi  33523  1arithidom  33565  fldext2chn  33769  constrconj  33786  constrfin  33787  constrelextdg2  33788  zarcmplem  33880  afsval  34686  dffltz  42644  smfmullem3  46808