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  18527  restmetu  24483  foresf1o  32479  2ndresdju  32626  nn0xmulclb  32749  gsumwrd2dccatlem  33041  isdrng4  33256  fracfld  33269  elrspunidl  33388  elrspunsn  33389  rhmpreimaprmidl  33411  1arithidom  33497  mplvrpmga  33570  fedgmul  33639  locfinreflem  33848  pstmxmet  33905  satfdmlem  35400  mblfinlem3  37698  itg2gt0cn  37714  dffltz  42666  pell1234qrmulcl  42887  suplesup  45377  limclner  45688  bgoldbtbnd  47839  gricushgr  47947