Theorem ad8antr 740

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad9antr  742  ad9antlr  743  simp-8l  790  legso  28671  miriso  28742  midexlem  28764  opphl  28826  trgcopy  28876  inaghl  28917  cyc3conja  33239  elrgspnlem4  33327  rloccring  33352  ssdifidlprm  33539  mxidlirred  33553  qsdrngi  33576  1arithidom  33618  1arithufdlem3  33627  lbsdiflsp0  33783  dimkerim  33784  fedgmul  33788  constrelextdg2  33904  qtophaus  33993  zarcmplem  34038  afsval  34828  dffltz  42877  hoidmvle  46844  smfmullem3  47037