Theorem ad8antr 753

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad9antr  755  ad9antlr  756  simp-8l  803  ssdifidlprm  21622  legso  29044  miriso  29124  midexlem  29146  opphl  29212  trgcopy  29293  inaghl  29346  cgraer  29359  angmgmaddeu1  29361  angmgmaddcpbl  29372  angmgmaddrid  29375  prlngmolem1  29412  prlngmolem2  29413  cyc3conja  33700  elrgspnlem4  33788  rloccring  33814  mxidlirred  33979  qsdrngi  34001  1arithidom  34051  1arithufdlem3  34060  lbsdiflsp0  34240  dimkerim  34241  fedgmul  34245  constrelextdg2  34361  qtophaus  34450  zarcmplem  34495  afsval  35286  dffltz  43624  hoidmvle  47554  smfmullem3  47747