Theorem ad8antr 741

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 739	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  743  ad9antlr  744  simp-8l  791  legso  28667  miriso  28738  midexlem  28760  opphl  28822  trgcopy  28872  inaghl  28913  cyc3conja  33218  elrgspnlem4  33306  rloccring  33331  ssdifidlprm  33518  mxidlirred  33532  qsdrngi  33555  1arithidom  33597  1arithufdlem3  33606  lbsdiflsp0  33770  dimkerim  33771  fedgmul  33775  constrelextdg2  33891  qtophaus  33980  zarcmplem  34025  afsval  34815  dffltz  43067  hoidmvle  47028  smfmullem3  47221