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  21555  legso  28949  miriso  29029  midexlem  29051  opphl  29117  trgcopy  29198  inaghl  29251  cgraer  29264  angmgmaddeu1  29266  angmgmaddcpbl  29277  angmgmaddrid  29280  prlngmolem1  29317  prlngmolem2  29318  cyc3conja  33605  elrgspnlem4  33693  rloccring  33719  mxidlirred  33883  qsdrngi  33905  1arithidom  33955  1arithufdlem3  33964  lbsdiflsp0  34144  dimkerim  34145  fedgmul  34149  constrelextdg2  34265  qtophaus  34354  zarcmplem  34399  afsval  35190  dffltz  43488  hoidmvle  47436  smfmullem3  47629