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  8077  chnso  18547  restmetu  24514  foresf1o  32579  2ndresdju  32727  nn0xmulclb  32851  gsumwrd2dccatlem  33159  isdrng4  33377  fracfld  33390  elrspunidl  33509  elrspunsn  33510  rhmpreimaprmidl  33532  1arithidom  33618  mplvrpmga  33710  fedgmul  33788  locfinreflem  33997  pstmxmet  34054  satfdmlem  35562  mblfinlem3  37856  itg2gt0cn  37872  dffltz  42873  pell1234qrmulcl  43093  suplesup  45580  limclner  45891  bgoldbtbnd  48051  gricushgr  48159