Theorem ad8antr 740

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 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad7antr 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:  ad9antr  742  ad9antlr  743  simp-8l  790  legso  28533  miriso  28604  midexlem  28626  opphl  28688  trgcopy  28738  inaghl  28779  cyc3conja  33121  elrgspnlem4  33203  rloccring  33228  ssdifidlprm  33436  mxidlirred  33450  qsdrngi  33473  1arithidom  33515  1arithufdlem3  33524  lbsdiflsp0  33629  dimkerim  33630  fedgmul  33634  constrelextdg2  33744  qtophaus  33833  zarcmplem  33878  afsval  34669  dffltz  42629  hoidmvle  46605  smfmullem3  46798