Theorem ad5antlr 748

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad5antlr	⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 487	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 745	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:  simp-5r  798  fimaproj  8137  chnso  18718  isdrng4  20908  rhmpreimaprmidl  21548  restmetu  24802  foresf1o  32987  2ndresdju  33130  nn0xmulclb  33250  gsumwrd2dccatlem  33525  fracfld  33757  elrspunidl  33864  elrspunsn  33865  1arithidom  33955  mplvrpmga  34063  fedgmul  34149  locfinreflem  34358  pstmxmet  34415  satfdmlem  35955  mblfinlem3  38416  itg2gt0cn  38432  dffltz  43488  pell1234qrmulcl  43704  suplesup  46177  limclner  46487  bgoldbtbnd  48733  gricushgr  48841