Theorem ad7antr 736

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad8antr  738  ad8antlr  739  simp-7l  787  catpropd  16962  natpropd  17229  ucncn  22877  tgcgrxfr  26290  tgbtwnconn1lem3  26346  tgbtwnconn1  26347  midexlem  26464  lnopp2hpgb  26535  trgcopy  26576  qsidomlem2  30976  lbsdiflsp0  31032  fedgmul  31037  sigapildsys  31428  afsval  31949  matunitlindflem1  34922  dffltz  39363