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  28562  miriso  28633  midexlem  28655  opphl  28717  trgcopy  28767  inaghl  28808  cyc3conja  33112  elrgspnlem4  33198  rloccring  33223  ssdifidlprm  33408  mxidlirred  33422  qsdrngi  33445  1arithidom  33487  1arithufdlem3  33496  lbsdiflsp0  33601  dimkerim  33602  fedgmul  33606  constrelextdg2  33716  qtophaus  33805  zarcmplem  33850  afsval  34641  dffltz  42610  hoidmvle  46585  smfmullem3  46778