Theorem ad8antr 738

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 479	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad7antr 736	1 ⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ad9antr  740  ad9antlr  741  simp-8l  789  legso  28568  miriso  28639  midexlem  28661  opphl  28723  trgcopy  28773  inaghl  28814  cyc3conja  33095  rloccring  33187  ssdifidlprm  33396  mxidlirred  33410  qsdrngi  33433  1arithidom  33475  1arithufdlem3  33484  lbsdiflsp0  33584  dimkerim  33585  fedgmul  33589  constrelextdg2  33682  qtophaus  33727  zarcmplem  33772  afsval  34593  dffltz  42399  hoidmvle  46332  smfmullem3  46525