Theorem ad8antr 741

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 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:  ad9antr  743  ad9antlr  744  simp-8l  791  legso  28683  miriso  28754  midexlem  28776  opphl  28838  trgcopy  28888  inaghl  28929  cyc3conja  33250  elrgspnlem4  33338  rloccring  33363  ssdifidlprm  33550  mxidlirred  33564  qsdrngi  33587  1arithidom  33629  1arithufdlem3  33638  lbsdiflsp0  33803  dimkerim  33804  fedgmul  33808  constrelextdg2  33924  qtophaus  34013  zarcmplem  34058  afsval  34848  dffltz  42989  hoidmvle  46955  smfmullem3  47148