Theorem ad7antr 744

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad8antr  746  ad8antlr  747  simp-7l  794  catpropd  17673  natpropd  17944  chnub  18586  ucncn  24274  tgcgrxfr  28611  tgbtwnconn1lem3  28667  tgbtwnconn1  28668  midexlem  28785  lnopp2hpgb  28856  trgcopy  28897  mgcf1o  33089  elrgspnlem4  33333  elrspunidl  33518  rhmimaidl  33522  qsidomlem2  33543  ssdifidlprm  33548  mxidlirredi  33561  1arithufdlem3  33636  lbsdiflsp0  33817  fedgmul  33822  constrconj  33936  constrelextdg2  33938  zarcmplem  34072  sigapildsys  34353  afsval  34862  matunitlindflem1  37990  aks6d1c2lem4  42619  dffltz  43091