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  8179  chnso  18827  isdrng4  21022  rhmpreimaprmidl  21665  restmetu  24919  foresf1o  33172  2ndresdju  33315  nn0xmulclb  33433  gsumwrd2dccatlem  33708  fracfld  33940  elrspunidl  34048  elrspunsn  34049  1arithidom  34139  mplvrpmga  34247  fedgmul  34333  locfinreflem  34542  pstmxmet  34599  satfdmlem  36300  mh-inf3f1  37507  mblfinlem3  38769  itg2gt0cn  38785  dffltz  43863  pell1234qrmulcl  44055  suplesup  46556  limclner  46866  bgoldbtbnd  49112  gricushgr  49220