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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad8antr  740  ad8antlr  741  simp-7l  789  catpropd  17166  natpropd  17439  ucncn  23136  tgcgrxfr  26563  tgbtwnconn1lem3  26619  tgbtwnconn1  26620  midexlem  26737  lnopp2hpgb  26808  trgcopy  26849  mgcf1o  30954  elrspunidl  31274  rhmimaidl  31277  qsidomlem2  31297  lbsdiflsp0  31375  fedgmul  31380  zarcmplem  31499  sigapildsys  31796  afsval  32317  matunitlindflem1  35459  dffltz  40115