Theorem simp-7r 789

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  17609  2sqmo  27404  tgbtwnconn1  28647  legso  28671  miriso  28742  footexALT  28790  footex  28793  opphl  28826  lnopp2hpgb  28835  f1otrg  28943  2ndresdju  32727  cyc3genpm  33234  cyc3conja  33239  rloccring  33352  isprmidlc  33528  ssdifidlprm  33539  mxidlprm  33551  qsdrngi  33576  1arithidom  33618  fldext2chn  33885  constrconj  33902  constrfin  33903  constrelextdg2  33904  zarcmplem  34038  afsval  34828  dffltz  42877  smfmullem3  47037  chnerlem1  47126