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  28587  miriso  28658  midexlem  28680  opphl  28742  trgcopy  28792  inaghl  28833  cyc3conja  33137  elrgspnlem4  33223  rloccring  33248  ssdifidlprm  33434  mxidlirred  33448  qsdrngi  33471  1arithidom  33513  1arithufdlem3  33522  lbsdiflsp0  33650  dimkerim  33651  fedgmul  33655  constrelextdg2  33771  qtophaus  33860  zarcmplem  33905  afsval  34695  dffltz  42742  hoidmvle  46712  smfmullem3  46905