Theorem ad5antlr 748

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 487	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 745	1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simp-5r  798  fimaproj  8136  chnso  18778  isdrng4  20972  rhmpreimaprmidl  21615  restmetu  24869  foresf1o  33082  2ndresdju  33225  nn0xmulclb  33345  gsumwrd2dccatlem  33620  fracfld  33852  elrspunidl  33960  elrspunsn  33961  1arithidom  34051  mplvrpmga  34159  fedgmul  34245  locfinreflem  34454  pstmxmet  34511  satfdmlem  36102  mh-inf3f1  37299  mblfinlem3  38545  itg2gt0cn  38561  dffltz  43624  pell1234qrmulcl  43815  suplesup  46295  limclner  46605  bgoldbtbnd  48851  gricushgr  48959