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  17633  natpropd  17904  ucncn  24188  tgcgrxfr  28481  tgbtwnconn1lem3  28537  tgbtwnconn1  28538  midexlem  28655  lnopp2hpgb  28726  trgcopy  28767  mgcf1o  32958  chnub  32967  elrgspnlem4  33195  elrspunidl  33375  rhmimaidl  33379  qsidomlem2  33400  ssdifidlprm  33405  mxidlirredi  33418  1arithufdlem3  33493  lbsdiflsp0  33598  fedgmul  33603  constrconj  33711  constrelextdg2  33713  zarcmplem  33847  sigapildsys  34128  afsval  34638  matunitlindflem1  37595  aks6d1c2lem4  42100  dffltz  42607