Theorem ad7antr 751

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 486	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad6antr 749	1 ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad8antr  753  ad8antlr  754  simp-7l  801  catpropd  17803  natpropd  18074  chnub  18716  qsidomlem2  21550  ssdifidlprm  21555  matunitlindflem1  22907  ucncn  24516  tgcgrxfr  28868  tgbtwnconn1lem3  28924  tgbtwnconn1  28925  midexlem  29051  lnopp2hpgb  29128  trgcopy  29198  tgaaddcpbl  29239  cgraer  29264  cgrabasimass  29265  angmgmaddeu1  29266  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddrid  29280  perpprlng  29315  prlngmolem1  29317  mgcf1o  33451  elrgspnlem4  33693  rlocisunit  33724  elrspunidl  33864  rhmimaidl  33868  mxidlirredi  33882  1arithufdlem3  33964  lbsdiflsp0  34144  fedgmul  34149  constrconj  34263  constrelextdg2  34265  zarcmplem  34399  sigapildsys  34681  afsval  35190  aks6d1c2lem4  43001  dffltz  43488