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  28681  miriso  28752  midexlem  28774  opphl  28836  trgcopy  28886  inaghl  28927  cyc3conja  33233  elrgspnlem4  33321  rloccring  33346  ssdifidlprm  33533  mxidlirred  33547  qsdrngi  33570  1arithidom  33612  1arithufdlem3  33621  lbsdiflsp0  33786  dimkerim  33787  fedgmul  33791  constrelextdg2  33907  qtophaus  33996  zarcmplem  34041  afsval  34831  dffltz  43081  hoidmvle  47046  smfmullem3  47239