Theorem ad5antlr 741

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 482	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 738	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:  simp-5r  791  fimaproj  8082  chnso  18588  restmetu  24560  foresf1o  32599  2ndresdju  32748  nn0xmulclb  32870  gsumwrd2dccatlem  33165  isdrng4  33386  fracfld  33399  elrspunidl  33518  elrspunsn  33519  rhmpreimaprmidl  33541  1arithidom  33627  mplvrpmga  33736  fedgmul  33822  locfinreflem  34031  pstmxmet  34088  satfdmlem  35603  mblfinlem3  38033  itg2gt0cn  38049  dffltz  43091  pell1234qrmulcl  43307  suplesup  45791  limclner  46101  bgoldbtbnd  48307  gricushgr  48415