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  8065  chnso  18530  restmetu  24485  foresf1o  32484  2ndresdju  32631  nn0xmulclb  32754  gsumwrd2dccatlem  33046  isdrng4  33261  fracfld  33274  elrspunidl  33393  elrspunsn  33394  rhmpreimaprmidl  33416  1arithidom  33502  mplvrpmga  33575  fedgmul  33644  locfinreflem  33853  pstmxmet  33910  satfdmlem  35412  mblfinlem3  37698  itg2gt0cn  37714  dffltz  42726  pell1234qrmulcl  42947  suplesup  45437  limclner  45748  bgoldbtbnd  47908  gricushgr  48016