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  17670  natpropd  17941  ucncn  24172  tgcgrxfr  28445  tgbtwnconn1lem3  28501  tgbtwnconn1  28502  midexlem  28619  lnopp2hpgb  28690  trgcopy  28731  mgcf1o  32929  chnub  32938  elrgspnlem4  33196  elrspunidl  33399  rhmimaidl  33403  qsidomlem2  33424  ssdifidlprm  33429  mxidlirredi  33442  1arithufdlem3  33517  lbsdiflsp0  33622  fedgmul  33627  constrconj  33735  constrelextdg2  33737  zarcmplem  33871  sigapildsys  34152  afsval  34662  matunitlindflem1  37610  aks6d1c2lem4  42115  dffltz  42622