Theorem ad7antr 737

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 735	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  739  ad8antlr  740  simp-7l  788  catpropd  17767  natpropd  18046  ucncn  24315  tgcgrxfr  28544  tgbtwnconn1lem3  28600  tgbtwnconn1  28601  midexlem  28718  lnopp2hpgb  28789  trgcopy  28830  mgcf1o  32976  chnub  32984  elrspunidl  33421  rhmimaidl  33425  qsidomlem2  33446  ssdifidlprm  33451  mxidlirredi  33464  1arithufdlem3  33539  lbsdiflsp0  33639  fedgmul  33644  constrconj  33735  constrelextdg2  33737  zarcmplem  33827  sigapildsys  34126  afsval  34648  matunitlindflem1  37576  aks6d1c2lem4  42084  dffltz  42589