Theorem ad7antr 738

Description: Deduction adding 7 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
ad7antr	⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Proof of Theorem ad7antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad6antr 736	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:  ad8antr  740  ad8antlr  741  simp-7l  788  catpropd  17617  natpropd  17888  chnub  18530  ucncn  24200  tgcgrxfr  28497  tgbtwnconn1lem3  28553  tgbtwnconn1  28554  midexlem  28671  lnopp2hpgb  28742  trgcopy  28783  mgcf1o  32991  elrgspnlem4  33219  elrspunidl  33400  rhmimaidl  33404  qsidomlem2  33425  ssdifidlprm  33430  mxidlirredi  33443  1arithufdlem3  33518  lbsdiflsp0  33660  fedgmul  33665  constrconj  33779  constrelextdg2  33781  zarcmplem  33915  sigapildsys  34196  afsval  34705  matunitlindflem1  37677  aks6d1c2lem4  42241  dffltz  42753