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  8161  restmetu  24584  foresf1o  32524  2ndresdju  32660  nn0xmulclb  32776  chnso  33005  gsumwrd2dccatlem  33070  isdrng4  33299  fracfld  33311  elrspunidl  33457  elrspunsn  33458  rhmpreimaprmidl  33480  1arithidom  33566  fedgmul  33683  locfinreflem  33840  pstmxmet  33897  satfdmlem  35374  mblfinlem3  37667  itg2gt0cn  37683  dffltz  42649  pell1234qrmulcl  42871  suplesup  45355  limclner  45671  bgoldbtbnd  47801  gricushgr  47891