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 481	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad6antr 734	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  738  ad8antlr  739  simp-7l  787  catpropd  17657  natpropd  17933  ucncn  24010  tgcgrxfr  28024  tgbtwnconn1lem3  28080  tgbtwnconn1  28081  midexlem  28198  lnopp2hpgb  28269  trgcopy  28310  mgcf1o  32428  elrspunidl  32808  rhmimaidl  32812  qsidomlem2  32834  mxidlirredi  32849  lbsdiflsp0  32987  fedgmul  32992  zarcmplem  33147  sigapildsys  33446  afsval  33969  matunitlindflem1  36787  dffltz  41678