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 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad6antr 736	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 207  df-an 396

This theorem is referenced by:  ad8antr  740  ad8antlr  741  simp-7l  788  catpropd  17721  natpropd  17992  ucncn  24223  tgcgrxfr  28497  tgbtwnconn1lem3  28553  tgbtwnconn1  28554  midexlem  28671  lnopp2hpgb  28742  trgcopy  28783  mgcf1o  32983  chnub  32992  elrgspnlem4  33240  elrspunidl  33443  rhmimaidl  33447  qsidomlem2  33468  ssdifidlprm  33473  mxidlirredi  33486  1arithufdlem3  33561  lbsdiflsp0  33666  fedgmul  33671  constrconj  33779  constrelextdg2  33781  zarcmplem  33912  sigapildsys  34193  afsval  34703  matunitlindflem1  37640  aks6d1c2lem4  42140  dffltz  42657