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  17677  natpropd  17948  ucncn  24179  tgcgrxfr  28452  tgbtwnconn1lem3  28508  tgbtwnconn1  28509  midexlem  28626  lnopp2hpgb  28697  trgcopy  28738  mgcf1o  32936  chnub  32945  elrgspnlem4  33203  elrspunidl  33406  rhmimaidl  33410  qsidomlem2  33431  ssdifidlprm  33436  mxidlirredi  33449  1arithufdlem3  33524  lbsdiflsp0  33629  fedgmul  33634  constrconj  33742  constrelextdg2  33744  zarcmplem  33878  sigapildsys  34159  afsval  34669  matunitlindflem1  37617  aks6d1c2lem4  42122  dffltz  42629