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  21647  legso  29067  miriso  29147  midexlem  29169  opphl  29235  trgcopy  29316  inaghl  29369  cgraer  29382  angmgmaddeu1  29384  angmgmaddcpbl  29395  angmgmaddrid  29398  prlngmolem1  29435  prlngmolem2  29436  cyc3conja  33764  elrgspnlem4  33852  rloccring  33878  mxidlirred  34043  qsdrngi  34065  1arithidom  34115  1arithufdlem3  34124  lbsdiflsp0  34304  dimkerim  34305  fedgmul  34309  constrelextdg2  34425  qtophaus  34514  zarcmplem  34559  afsval  35349  dffltz  43763  hoidmvle  47703  smfmullem3  47896