Theorem ad7antr 735

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 481	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad6antr 733	1 ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ad8antr  737  ad8antlr  738  simp-7l  786  catpropd  17418  natpropd  17694  ucncn  23437  tgcgrxfr  26879  tgbtwnconn1lem3  26935  tgbtwnconn1  26936  midexlem  27053  lnopp2hpgb  27124  trgcopy  27165  mgcf1o  31281  elrspunidl  31606  rhmimaidl  31609  qsidomlem2  31629  lbsdiflsp0  31707  fedgmul  31712  zarcmplem  31831  sigapildsys  32130  afsval  32651  matunitlindflem1  35773  dffltz  40471