Theorem ad8antr 750

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad9antr  752  ad9antlr  753  simp-8l  800  legso  28745  miriso  28816  midexlem  28838  opphl  28900  trgcopy  28950  inaghl  28991  cyc3conja  33298  elrgspnlem4  33387  rloccring  33413  ssdifidlprm  33606  mxidlirred  33621  qsdrngi  33644  1arithidom  33694  1arithufdlem3  33703  lbsdiflsp0  33884  dimkerim  33885  fedgmul  33889  constrelextdg2  34005  qtophaus  34094  zarcmplem  34139  afsval  34932  dffltz  43180  hoidmvle  47138  smfmullem3  47331