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  28526  miriso  28597  midexlem  28619  opphl  28681  trgcopy  28731  inaghl  28772  cyc3conja  33114  elrgspnlem4  33196  rloccring  33221  ssdifidlprm  33429  mxidlirred  33443  qsdrngi  33466  1arithidom  33508  1arithufdlem3  33517  lbsdiflsp0  33622  dimkerim  33623  fedgmul  33627  constrelextdg2  33737  qtophaus  33826  zarcmplem  33871  afsval  34662  dffltz  42622  hoidmvle  46598  smfmullem3  46791