Theorem ad8antr 746

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad9antr  748  ad9antlr  749  simp-8l  796  legso  28692  miriso  28763  midexlem  28785  opphl  28847  trgcopy  28897  inaghl  28938  cyc3conja  33245  elrgspnlem4  33333  rloccring  33358  ssdifidlprm  33548  mxidlirred  33562  qsdrngi  33585  1arithidom  33627  1arithufdlem3  33636  lbsdiflsp0  33817  dimkerim  33818  fedgmul  33822  constrelextdg2  33938  qtophaus  34027  zarcmplem  34072  afsval  34862  dffltz  43091  hoidmvle  47050  smfmullem3  47243