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  17888  natpropd  18159  chnub  18801  qsidomlem2  21642  ssdifidlprm  21647  matunitlindflem1  22999  ucncn  24608  tgcgrxfr  28986  tgbtwnconn1lem3  29042  tgbtwnconn1  29043  midexlem  29169  lnopp2hpgb  29246  trgcopy  29316  tgaaddcpbl  29357  cgraer  29382  cgrabasimass  29383  angmgmaddeu1  29384  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddrid  29398  perpprlng  29433  prlngmolem1  29435  mgcf1o  33610  elrgspnlem4  33852  rlocisunit  33883  elrspunidl  34024  rhmimaidl  34028  mxidlirredi  34042  1arithufdlem3  34124  lbsdiflsp0  34304  fedgmul  34309  constrconj  34423  constrelextdg2  34425  zarcmplem  34559  sigapildsys  34841  afsval  35349  aks6d1c2lem4  43270  dffltz  43763