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  17731  2sqmo  27496  tgbtwnconn1  28598  legso  28622  miriso  28693  footexALT  28741  footex  28744  opphl  28777  lnopp2hpgb  28786  f1otrg  28894  2ndresdju  32666  cyc3genpm  33155  cyc3conja  33160  rloccring  33257  isprmidlc  33455  ssdifidlprm  33466  mxidlprm  33478  qsdrngi  33503  1arithidom  33545  fldext2chn  33734  constrconj  33750  constrfin  33751  constrelextdg2  33752  zarcmplem  33842  afsval  34665  dffltz  42621  smfmullem3  46749