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  8075  restmetu  24474  foresf1o  32466  2ndresdju  32606  nn0xmulclb  32727  chnso  32969  gsumwrd2dccatlem  33032  isdrng4  33244  fracfld  33257  elrspunidl  33375  elrspunsn  33376  rhmpreimaprmidl  33398  1arithidom  33484  fedgmul  33603  locfinreflem  33806  pstmxmet  33863  satfdmlem  35340  mblfinlem3  37638  itg2gt0cn  37654  dffltz  42607  pell1234qrmulcl  42828  suplesup  45319  limclner  45633  bgoldbtbnd  47794  gricushgr  47902