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  8085  chnso  18590  restmetu  24535  foresf1o  32574  2ndresdju  32722  nn0xmulclb  32844  gsumwrd2dccatlem  33138  isdrng4  33356  fracfld  33369  elrspunidl  33488  elrspunsn  33489  rhmpreimaprmidl  33511  1arithidom  33597  mplvrpmga  33689  fedgmul  33775  locfinreflem  33984  pstmxmet  34041  satfdmlem  35550  mblfinlem3  37980  itg2gt0cn  37996  dffltz  43067  pell1234qrmulcl  43283  suplesup  45769  limclner  46079  bgoldbtbnd  48285  gricushgr  48393