Theorem ad7antr 734

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 732	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 206  df-an 396

This theorem is referenced by:  ad8antr  736  ad8antlr  737  simp-7l  785  catpropd  17335  natpropd  17610  ucncn  23345  tgcgrxfr  26783  tgbtwnconn1lem3  26839  tgbtwnconn1  26840  midexlem  26957  lnopp2hpgb  27028  trgcopy  27069  mgcf1o  31183  elrspunidl  31508  rhmimaidl  31511  qsidomlem2  31531  lbsdiflsp0  31609  fedgmul  31614  zarcmplem  31733  sigapildsys  32030  afsval  32551  matunitlindflem1  35700  dffltz  40387