Theorem simp-8r 797

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-8r	⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Proof of Theorem simp-8r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad8antlr 747	1 ⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  chnso  18588  2sqmo  27425  legso  28692  opphl  28847  f1otrg  28964  2ndresdju  32748  cyc3conja  33245  rloccring  33358  ssdifidlprm  33548  mxidlprm  33560  mxidlirred  33562  constrconj  33936  constrfin  33937  constrelextdg2  33938  cos9thpiminplylem2  33974  qtophaus  34027  esumcst  34254  dffltz  43091  smfmullem3  47243