Theorem ad7antr 748

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad8antr  750  ad8antlr  751  simp-7l  798  catpropd  17724  natpropd  17995  chnub  18637  ucncn  24324  tgcgrxfr  28664  tgbtwnconn1lem3  28720  tgbtwnconn1  28721  midexlem  28838  lnopp2hpgb  28909  trgcopy  28950  mgcf1o  33142  elrgspnlem4  33387  rlocisunit  33418  elrspunidl  33575  rhmimaidl  33579  qsidomlem2  33601  ssdifidlprm  33606  mxidlirredi  33620  1arithufdlem3  33703  lbsdiflsp0  33884  fedgmul  33889  constrconj  34003  constrelextdg2  34005  zarcmplem  34139  sigapildsys  34420  afsval  34932  matunitlindflem1  38079  aks6d1c2lem4  42708  dffltz  43180