Theorem ad7antr 750

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad8antr  752  ad8antlr  753  simp-7l  800  catpropd  17755  natpropd  18026  chnub  18668  qsidomlem2  21441  ssdifidlprm  21446  ucncn  24402  tgcgrxfr  28745  tgbtwnconn1lem3  28801  tgbtwnconn1  28802  midexlem  28923  lnopp2hpgb  28994  trgcopy  29056  mgcf1o  33236  elrgspnlem4  33478  rlocisunit  33509  elrspunidl  33652  rhmimaidl  33656  mxidlirredi  33671  1arithufdlem3  33753  lbsdiflsp0  33933  fedgmul  33938  constrconj  34052  constrelextdg2  34054  zarcmplem  34188  sigapildsys  34469  afsval  34978  matunitlindflem1  38127  aks6d1c2lem4  42756  dffltz  43228