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  21675  legso  29095  miriso  29175  midexlem  29197  opphl  29263  trgcopy  29344  inaghl  29397  cgraer  29410  angmgmaddeu1  29412  angmgmaddcpbl  29423  angmgmaddrid  29426  prlngmolem1  29463  prlngmolem2  29464  cyc3conja  33794  elrgspnlem4  33882  rloccring  33908  mxidlirred  34081  qsdrngi  34103  1arithidom  34153  1arithufdlem3  34162  lbsdiflsp0  34341  dimkerim  34342  fedgmul  34346  constrelextdg2  34462  qtophaus  34551  zarcmplem  34596  afsval  35386  dffltz  43874  hoidmvle  47825  smfmullem3  48018