Theorem ad8antr 752

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad9antr  754  ad9antlr  755  simp-8l  802  ssdifidlprm  21446  legso  28826  miriso  28901  midexlem  28923  opphl  28985  trgcopy  29056  inaghl  29097  cyc3conja  33390  elrgspnlem4  33478  rloccring  33504  mxidlirred  33672  qsdrngi  33694  1arithidom  33744  1arithufdlem3  33753  lbsdiflsp0  33933  dimkerim  33934  fedgmul  33938  constrelextdg2  34054  qtophaus  34143  zarcmplem  34188  afsval  34978  dffltz  43228  hoidmvle  47172  smfmullem3  47365