Theorem ad5antlr 735

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 732	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  785  fimaproj  8071  chnso  18532  restmetu  24486  foresf1o  32486  2ndresdju  32633  nn0xmulclb  32758  gsumwrd2dccatlem  33053  isdrng4  33268  fracfld  33281  elrspunidl  33400  elrspunsn  33401  rhmpreimaprmidl  33423  1arithidom  33509  mplvrpmga  33593  fedgmul  33665  locfinreflem  33874  pstmxmet  33931  satfdmlem  35433  mblfinlem3  37719  itg2gt0cn  37735  dffltz  42752  pell1234qrmulcl  42972  suplesup  45462  limclner  45773  bgoldbtbnd  47933  gricushgr  48041