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 738	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  17744  2sqmo  27499  tgbtwnconn1  28601  legso  28625  miriso  28696  footexALT  28744  footex  28747  opphl  28780  lnopp2hpgb  28789  f1otrg  28897  2ndresdju  32667  cyc3genpm  33145  cyc3conja  33150  rloccring  33242  isprmidlc  33440  ssdifidlprm  33451  mxidlprm  33463  qsdrngi  33488  1arithidom  33530  fldext2chn  33719  constrconj  33735  constrfin  33736  constrelextdg2  33737  zarcmplem  33827  afsval  34648  dffltz  42589  smfmullem3  46714