Theorem ad8antr 753

Description: Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad8antr	⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)

Proof of Theorem ad8antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad7antr 751	1 ⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad9antr  755  ad9antlr  756  simp-8l  803  ssdifidlprm  21523  legso  28905  miriso  28984  midexlem  29006  opphl  29072  trgcopy  29152  inaghl  29199  prlngmolem1  29239  prlngmolem2  29240  cyc3conja  33508  elrgspnlem4  33596  rloccring  33622  mxidlirred  33786  qsdrngi  33808  1arithidom  33858  1arithufdlem3  33867  lbsdiflsp0  34047  dimkerim  34048  fedgmul  34052  constrelextdg2  34168  qtophaus  34257  zarcmplem  34302  afsval  35093  dffltz  43407  hoidmvle  47355  smfmullem3  47548