Theorem ad5antlr 736

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simp-5r  786  fimaproj  8078  chnso  18581  restmetu  24545  foresf1o  32589  2ndresdju  32737  nn0xmulclb  32859  gsumwrd2dccatlem  33153  isdrng4  33371  fracfld  33384  elrspunidl  33503  elrspunsn  33504  rhmpreimaprmidl  33526  1arithidom  33612  mplvrpmga  33704  fedgmul  33791  locfinreflem  34000  pstmxmet  34057  satfdmlem  35566  mblfinlem3  37994  itg2gt0cn  38010  dffltz  43081  pell1234qrmulcl  43301  suplesup  45787  limclner  46097  bgoldbtbnd  48297  gricushgr  48405