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  21467  legso  28849  miriso  28928  midexlem  28950  opphl  29016  trgcopy  29096  inaghl  29143  prlngmolem1  29183  prlngmolem2  29184  cyc3conja  33458  elrgspnlem4  33546  rloccring  33572  mxidlirred  33736  qsdrngi  33758  1arithidom  33808  1arithufdlem3  33817  lbsdiflsp0  33997  dimkerim  33998  fedgmul  34002  constrelextdg2  34118  qtophaus  34207  zarcmplem  34252  afsval  35042  dffltz  43349  hoidmvle  47297  smfmullem3  47490