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  8140  chnso  18705  isdrng4  20876  rhmpreimaprmidl  21516  restmetu  24764  foresf1o  32887  2ndresdju  33031  nn0xmulclb  33153  gsumwrd2dccatlem  33428  fracfld  33660  elrspunidl  33767  elrspunsn  33768  1arithidom  33858  mplvrpmga  33966  fedgmul  34052  locfinreflem  34261  pstmxmet  34318  satfdmlem  35881  mblfinlem3  38351  itg2gt0cn  38367  dffltz  43407  pell1234qrmulcl  43623  suplesup  46096  limclner  46406  bgoldbtbnd  48615  gricushgr  48723