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  17592  2sqmo  27376  tgbtwnconn1  28554  legso  28578  miriso  28649  footexALT  28697  footex  28700  opphl  28733  lnopp2hpgb  28742  f1otrg  28850  2ndresdju  32629  cyc3genpm  33119  cyc3conja  33124  rloccring  33235  isprmidlc  33410  ssdifidlprm  33421  mxidlprm  33433  qsdrngi  33458  1arithidom  33500  fldext2chn  33739  constrconj  33756  constrfin  33757  constrelextdg2  33758  zarcmplem  33892  afsval  34682  dffltz  42673  smfmullem3  46837