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  8154  chnso  18803  isdrng4  20997  rhmpreimaprmidl  21640  restmetu  24894  foresf1o  33147  2ndresdju  33290  nn0xmulclb  33409  gsumwrd2dccatlem  33684  fracfld  33916  elrspunidl  34024  elrspunsn  34025  1arithidom  34115  mplvrpmga  34223  fedgmul  34309  locfinreflem  34518  pstmxmet  34575  satfdmlem  36219  mh-inf3f1  37421  mblfinlem3  38670  itg2gt0cn  38686  dffltz  43763  pell1234qrmulcl  43955  suplesup  46444  limclner  46754  bgoldbtbnd  49000  gricushgr  49108